# 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
         ];