| changeset 57945 | cacb00a569e0 |
| parent 56511 | 265816f87386 |
| child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/Domain_Aux.thy Fri Aug 15 18:02:34 2014 +0200 +++ b/src/HOL/HOLCF/Domain_Aux.thy Sat Aug 16 11:35:33 2014 +0200 @@ -344,6 +344,9 @@ subsection {* ML setup *} +named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)" +named_theorems domain_map_ID "theorems like foo_map$ID = ID" + ML_file "Tools/Domain/domain_take_proofs.ML" ML_file "Tools/cont_consts.ML" ML_file "Tools/cont_proc.ML"