diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Fix.ML	Thu May 31 16:52:32 2001 +0200
@@ -20,7 +20,7 @@
 (* This property is essential since monotonicity of iterate makes no sense  *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [chain]  "x << F$x ==> chain (%i. iterate i F x)";
+Goalw [chain_def]  "x << F$x ==> chain (%i. iterate i F x)";
 by (strip_tac 1);
 by (induct_tac "i" 1);
 by Auto_tac;  
@@ -28,7 +28,7 @@
 qed "chain_iterate2";
 
 
-Goal   "chain (%i. iterate i F UU)";
+Goal "chain (%i. iterate i F UU)";
 by (rtac chain_iterate2 1);
 by (rtac minimal 1);
 qed "chain_iterate";
@@ -350,10 +350,15 @@
 (* ------------------------------------------------------------------------ *)
 
 val prems = Goalw [adm_def]
-   "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)";
+   "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P";
 by (blast_tac (claset() addIs prems) 1);
 qed "admI";
 
+Goal "!x. P x ==> adm P";
+by (rtac admI 1);
+by (etac spec 1);
+qed "triv_admI";
+
 Goalw [adm_def] "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))";
 by (Blast_tac 1);
 qed "admD";
@@ -558,7 +563,7 @@
 by (force_tac (claset() addEs [admD], simpset()) 1);
 qed "adm_disj_lemma2";
 
-Goalw [chain] "chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)";
+Goalw [chain_def]"chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)";
 by (Asm_simp_tac 1);
 by (safe_tac HOL_cs);
 by (subgoal_tac "ia = i" 1);
@@ -722,7 +727,7 @@
 by (atac 1);
 qed "adm_not_conj";
 
-bind_thms ("adm_lemmas", [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
-        adm_all2,adm_not_less,adm_not_conj,adm_iff]);
+bind_thms ("adm_lemmas", [adm_not_free,adm_imp,adm_disj,adm_eq,adm_not_UU,
+        adm_UU_not_less,adm_all2,adm_not_less,adm_not_conj,adm_iff]);
 
 Addsimps adm_lemmas;