src/HOL/WF_Rel.ML

--- a/src/HOL/WF_Rel.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -106,14 +106,14 @@
  *---------------------------------------------------------------------------*)
 
 goal thy "!!r. finite r ==> acyclic r --> wf r";
-be finite_induct 1;
- by(Blast_tac 1);
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (etac finite_induct 1);
+ by (Blast_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
 qed_spec_mp "finite_acyclic_wf";
 
 goal thy "!!r. finite r ==> wf r = acyclic r";
-by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
+by (blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
 qed "wf_iff_acyclic_if_finite";
 
 
@@ -123,26 +123,26 @@
 
 goalw thy [wf_eq_minimal RS eq_reflection]
   "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
-br iffI 1;
- br notI 1;
- be exE 1;
- by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
- by(Blast_tac 1);
-be swap 1;
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac swap 1);
 by (Asm_full_simp_tac 1);
 by (Step_tac 1);
-by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- br allI 1;
- by(Simp_tac 1);
- br selectI2EX 1;
-  by(Blast_tac 1);
- by(Blast_tac 1);
-br allI 1;
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(Simp_tac 1);
-br selectI2EX 1;
- by(Blast_tac 1);
-by(Blast_tac 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac selectI2EX 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac selectI2EX 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_iff_no_infinite_down_chain";