src/HOL/AxClasses/Lattice/CLattice.ML

--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -56,14 +56,14 @@
   by (cut_facts_tac prems 1);
   br selectI2 1;
   br Inf_is_Inf 1;
-  by (rewrite_goals_tac [is_Inf_def]);
+  by (rewtac is_Inf_def);
   by (fast_tac set_cs 1);
 qed "Inf_lb";
 
 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
   br selectI2 1;
   br Inf_is_Inf 1;
-  by (rewrite_goals_tac [is_Inf_def]);
+  by (rewtac is_Inf_def);
   by (step_tac HOL_cs 1);
   by (step_tac HOL_cs 1);
   be mp 1;
@@ -76,14 +76,14 @@
   by (cut_facts_tac prems 1);
   br selectI2 1;
   br Sup_is_Sup 1;
-  by (rewrite_goals_tac [is_Sup_def]);
+  by (rewtac is_Sup_def);
   by (fast_tac set_cs 1);
 qed "Sup_ub";
 
 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
   br selectI2 1;
   br Sup_is_Sup 1;
-  by (rewrite_goals_tac [is_Sup_def]);
+  by (rewtac is_Sup_def);
   by (step_tac HOL_cs 1);
   by (step_tac HOL_cs 1);
   be mp 1;
@@ -126,7 +126,7 @@
 goal thy "A <= B --> Inf B [= Inf A";
   br impI 1;
   by (stac le_Inf_eq 1);
-  by (rewrite_goals_tac [Ball_def]);
+  by (rewtac Ball_def);
   by (safe_tac set_cs);
   bd subsetD 1;
   ba 1;
@@ -136,7 +136,7 @@
 goal thy "A <= B --> Sup A [= Sup B";
   br impI 1;
   by (stac ge_Sup_eq 1);
-  by (rewrite_goals_tac [Ball_def]);
+  by (rewtac Ball_def);
   by (safe_tac set_cs);
   bd subsetD 1;
   ba 1;
@@ -148,7 +148,7 @@
 
 goal thy "Inf {x} = x";
   br (Inf_uniq RS mp) 1;
-  by (rewrite_goals_tac [is_Inf_def]);
+  by (rewtac is_Inf_def);
   by (safe_tac set_cs);
   br le_refl 1;
   by (fast_tac set_cs 1);
@@ -156,7 +156,7 @@
 
 goal thy "Sup {x} = x";
   br (Sup_uniq RS mp) 1;
-  by (rewrite_goals_tac [is_Sup_def]);
+  by (rewtac is_Sup_def);
   by (safe_tac set_cs);
   br le_refl 1;
   by (fast_tac set_cs 1);
@@ -165,7 +165,7 @@
 
 goal thy "Inf {} = Sup {x. True}";
   br (Inf_uniq RS mp) 1;
-  by (rewrite_goals_tac [is_Inf_def]);
+  by (rewtac is_Inf_def);
   by (safe_tac set_cs);
   br (sing_Sup_eq RS subst) 1;
   back();
@@ -175,7 +175,7 @@
 
 goal thy "Sup {} = Inf {x. True}";
   br (Sup_uniq RS mp) 1;
-  by (rewrite_goals_tac [is_Sup_def]);
+  by (rewtac is_Sup_def);
   by (safe_tac set_cs);
   br (sing_Inf_eq RS subst) 1;
   br (Inf_subset_antimon RS mp) 1;