src/HOL/Induct/Acc.ML
changeset 5223 4cb05273f764
parent 5168 adafef6eb295
child 5580 354f4914811f
--- a/src/HOL/Induct/Acc.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -9,8 +9,6 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-open Acc;
-
 (*The intended introduction rule*)
 val prems = goal Acc.thy
     "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
@@ -46,25 +44,25 @@
 qed "acc_induct";
 
 
-val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
-by (rtac (major RS wfI) 1);
+Goal "r <= (acc r) Times (acc r) ==> wf(r)";
+by (etac wfI 1);
 by (etac acc.induct 1);
 by (rewtac pred_def);
 by (Fast_tac 1);
 qed "acc_wfI";
 
-val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
-by (rtac (major RS wf_induct) 1);
+Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
+by (etac wf_induct 1);
 by (rtac (impI RS allI) 1);
 by (rtac accI 1);
 by (Fast_tac 1);
 qed "acc_wfD_lemma";
 
-val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
+Goal "wf(r) ==> r <= (acc r) Times (acc r)";
 by (rtac subsetI 1);
 by (res_inst_tac [("p", "x")] PairE 1);
 by (fast_tac (claset() addSIs [SigmaI,
-                             major RS acc_wfD_lemma RS spec RS mp]) 1);
+			       acc_wfD_lemma RS spec RS mp]) 1);
 qed "acc_wfD";
 
 Goal "wf(r)  =  (r <= (acc r) Times (acc r))";