# HG changeset patch # User oheimb # Date 837612222 -7200 # Node ID 206553e1a242d5c6b2b21262bf89983acf08264a # Parent 82246f607d7f2e93e8d24ff8b9f0558df3879312 renamed adm_impl to adm_imp diff -r 82246f607d7f -r 206553e1a242 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Wed Jul 17 15:25:50 1996 +0200 +++ b/src/HOLCF/Fix.ML Wed Jul 17 16:03:42 1996 +0200 @@ -1163,7 +1163,7 @@ ]); -qed_goal "adm_impl" Fix.thy +qed_goal "adm_imp" Fix.thy "[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)" (fn prems => [ @@ -1206,7 +1206,7 @@ fast_tac (HOL_cs addDs [le_imp_less_or_eq] addEs [chain_mono RS mp]) 1]); -val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, +val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less ];