diff -r 825877190618 -r 74919e8f221c src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/WF.ML	Wed Jul 15 14:19:02 1998 +0200
@@ -79,7 +79,7 @@
 val lemma1 = result();
 
 Goalw [wf_def]
-    "!!r. (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
+    "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
 by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
 by (Blast_tac 1);
@@ -140,7 +140,7 @@
 "!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]);
 
 Goalw [acyclic_def]
- "!!r. wf r ==> acyclic r";
+ "wf r ==> acyclic r";
 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
 qed "wf_acyclic";
 
@@ -171,7 +171,7 @@
 (*** is_recfun ***)
 
 Goalw [is_recfun_def,cut_def]
-    "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
+    "[| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
 by (etac ssubst 1);
 by (asm_simp_tac HOL_ss 1);
 qed "is_recfun_undef";
@@ -261,7 +261,7 @@
                      (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
 
 Goalw [wfrec_def]
-    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
 by (rtac H_cong 1);
 by (rtac refl 2);
 by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
@@ -297,7 +297,7 @@
 
 (*--------------Old proof-----------------------------------------------------
 Goalw [wfrec_def]
-    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
 by (etac (wf_trancl RS wftrec RS ssubst) 1);
 by (rtac trans_trancl 1);
 by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)