1.1 --- a/src/HOLCF/Fix.ML	Wed Jul 17 15:25:50 1996 +0200
     1.2 +++ b/src/HOLCF/Fix.ML	Wed Jul 17 16:03:42 1996 +0200
     1.3 @@ -1163,7 +1163,7 @@
     1.4          ]);
     1.5  
     1.6  
     1.7 -qed_goal "adm_impl"  Fix.thy  
     1.8 +qed_goal "adm_imp"  Fix.thy  
     1.9          "[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
    1.10   (fn prems =>
    1.11          [
    1.12 @@ -1206,7 +1206,7 @@
    1.13  	fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
    1.14  			 addEs [chain_mono RS mp]) 1]);
    1.15  
    1.16 -val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
    1.17 +val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
    1.18          adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less
    1.19          ];
    1.20