Changeset 2222
- Timestamp:
- Jul 20, 2012, 10:58:15 AM (9 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyFront.ma
r2221 r2222 431 431 Some ? (pi1 ?? final_policy). 432 432 [ / by I/ 433 | lapply p -p generalize in match (foldl_strong ?????); *#p #Hp #hg433 | lapply p -p cases final_policy -final_policy #p #Hp #hg 434 434 @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ] 435 435 | @conj [ @conj [ @conj [ @conj -
src/common/Identifiers.ma
r2182 r2222 809 809 [ #_ % 810 810 | #x #l' #Hi 811 whd in match ( l'@[x] : identifier_map tag unit);811 whd in match (set_from_list … (l'@[x])); 812 812 >foldl_append 813 813 #H @All_append … … 831 831 lapply (All_append_r … H) 832 832 * #Px * #Pl' #i 833 whd in match ( l'@[x] : identifier_map ??);833 whd in match (set_from_list … (l'@[x])); 834 834 >foldl_append 835 835 >mem_set_add … … 850 850 | #EQ >EQ * #ABS @ABS % 851 851 ] qed. 852 853 854
Note: See TracChangeset
for help on using the changeset viewer.