equal
deleted
inserted
replaced
315 by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map) |
315 by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map) |
316 |
316 |
317 subsection {* Setting up the domain package *} |
317 subsection {* Setting up the domain package *} |
318 |
318 |
319 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)" |
319 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)" |
320 named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" |
320 and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" |
321 |
321 |
322 ML_file "Tools/Domain/domain_isomorphism.ML" |
322 ML_file "Tools/Domain/domain_isomorphism.ML" |
323 ML_file "Tools/Domain/domain_axioms.ML" |
323 ML_file "Tools/Domain/domain_axioms.ML" |
324 ML_file "Tools/Domain/domain.ML" |
324 ML_file "Tools/Domain/domain.ML" |
325 |
325 |