equal
deleted
inserted
replaced
342 ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up |
342 ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up |
343 deflation_strict deflation_ID ID1 cfcomp2 |
343 deflation_strict deflation_ID ID1 cfcomp2 |
344 |
344 |
345 subsection {* ML setup *} |
345 subsection {* ML setup *} |
346 |
346 |
|
347 named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)" |
|
348 named_theorems domain_map_ID "theorems like foo_map$ID = ID" |
|
349 |
347 ML_file "Tools/Domain/domain_take_proofs.ML" |
350 ML_file "Tools/Domain/domain_take_proofs.ML" |
348 ML_file "Tools/cont_consts.ML" |
351 ML_file "Tools/cont_consts.ML" |
349 ML_file "Tools/cont_proc.ML" |
352 ML_file "Tools/cont_proc.ML" |
350 ML_file "Tools/Domain/domain_constructors.ML" |
353 ML_file "Tools/Domain/domain_constructors.ML" |
351 ML_file "Tools/Domain/domain_induction.ML" |
354 ML_file "Tools/Domain/domain_induction.ML" |