src/HOL/Lex/Prefix.ML

--- a/src/HOL/Lex/Prefix.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -15,18 +15,18 @@
 (** <= is a partial order: **)
 
 Goalw [prefix_def] "xs <= (xs::'a list)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "prefix_refl";
 AddIffs[prefix_refl];
 
 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
-by(Clarify_tac 1);
-by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
 qed "prefix_trans";
 
 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
 qed "prefix_antisym";
 
 (** recursion equations **)
@@ -44,17 +44,17 @@
 Addsimps [prefix_Nil];
 
 Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
-br iffI 1;
- be exE 1;
- by(rename_tac "zs" 1);
- by(res_inst_tac [("xs","zs")] rev_exhaust 1);
-  by(Asm_full_simp_tac 1);
- by(hyp_subst_tac 1);
- by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (rtac iffI 1);
+ by (etac exE 1);
+ by (rename_tac "zs" 1);
+ by (res_inst_tac [("xs","zs")] rev_exhaust 1);
+  by (Asm_full_simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
-be disjE 1;
- by(Asm_simp_tac 1);
-by(Clarify_tac 1);
+by (etac disjE 1);
+ by (Asm_simp_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 qed "prefix_snoc";
 Addsimps [prefix_snoc];
@@ -67,7 +67,7 @@
 
 Goal "(xs@ys <= xs@zs) = (ys <= zs)";
 by (induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "same_prefix_prefix";
 Addsimps [same_prefix_prefix];
 
@@ -75,7 +75,7 @@
  [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
 
 Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 qed "prefix_prefix";
 Addsimps [prefix_prefix];
@@ -90,11 +90,11 @@
 qed "prefix_Cons";
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by(res_inst_tac [("xs","zs")] rev_induct 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (res_inst_tac [("xs","zs")] rev_induct 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                 addsimps [append_assoc RS sym])1);
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "prefix_append";