# HG changeset patch
# User paulson
# Date 861787109 -7200
# Node ID 01364e2f30adbe3d08756afc98377bdbaf2d127f
# Parent  7ffe67afeb94847d25bd7431965949c515c534f9
Ran expandshort

diff -r 7ffe67afeb94 -r 01364e2f30ad src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -67,24 +67,24 @@
 goal thy
   "wp (WHILE b DO c) Q s = \
 \  (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
-by(simp_tac (!simpset setloop(split_tac[expand_if])) 1);
-br iffI 1;
- br weak_coinduct 1;
-  by(etac CollectI 1);
- by(safe_tac (!claset));
-  by(rotate_tac ~1 1);
-  by(Asm_full_simp_tac 1);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
-by(asm_full_simp_tac (!simpset addsimps [wp_def,Gamma_def]) 1);
-by(strip_tac 1);
-br mp 1;
- ba 2;
-be induct2 1;
-by(fast_tac (!claset addSIs [monoI]) 1);
-by(stac gfp_Tarski 1);
- by(fast_tac (!claset addSIs [monoI]) 1);
-by(Fast_tac 1);
+by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
+by (rtac iffI 1);
+ by (rtac weak_coinduct 1);
+  by (etac CollectI 1);
+ by (safe_tac (!claset));
+  by (rotate_tac ~1 1);
+  by (Asm_full_simp_tac 1);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [wp_def,Gamma_def]) 1);
+by (strip_tac 1);
+by (rtac mp 1);
+ by (assume_tac 2);
+by (etac induct2 1);
+by (fast_tac (!claset addSIs [monoI]) 1);
+by (stac gfp_Tarski 1);
+ by (fast_tac (!claset addSIs [monoI]) 1);
+by (Fast_tac 1);
 qed "wp_While";
 
 Delsimps [C_while];
diff -r 7ffe67afeb94 -r 01364e2f30ad src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/IMP/Transition.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -194,7 +194,7 @@
 goal Transition.thy 
   "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
 by (etac evalc1.induct 1);
-auto();
+by (Auto_tac());
 qed_spec_mp "FB_lemma3";
 
 val [major] = goal Transition.thy
diff -r 7ffe67afeb94 -r 01364e2f30ad src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/Nat.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -5,18 +5,18 @@
 *)
 
 goal thy "min 0 n = 0";
-br min_leastL 1;
-by(trans_tac 1);
+by (rtac min_leastL 1);
+by (trans_tac 1);
 qed "min_0L";
 
 goal thy "min n 0 = 0";
-br min_leastR 1;
-by(trans_tac 1);
+by (rtac min_leastR 1);
+by (trans_tac 1);
 qed "min_0R";
 
 goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
-by(split_tac [expand_if] 1);
-by(Simp_tac 1);
+by (split_tac [expand_if] 1);
+by (Simp_tac 1);
 qed "min_Suc_Suc";
 
 Addsimps [min_0L,min_0R,min_Suc_Suc];
diff -r 7ffe67afeb94 -r 01364e2f30ad src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -377,21 +377,21 @@
 
 qed_goal "nat_induct2" thy 
 "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
-	cut_facts_tac prems 1,
-	rtac less_induct 1,
-	res_inst_tac [("n","n")] natE 1,
-	 hyp_subst_tac 1,
-	 atac 1,
-	hyp_subst_tac 1,
-	res_inst_tac [("n","x")] natE 1,
-	 hyp_subst_tac 1,
-	 atac 1,
-	hyp_subst_tac 1,
-	resolve_tac prems 1,
-	dtac spec 1,
-	etac mp 1,
-	rtac (lessI RS less_trans) 1,
-	rtac (lessI RS Suc_mono) 1]);
+        cut_facts_tac prems 1,
+        rtac less_induct 1,
+        res_inst_tac [("n","n")] natE 1,
+         hyp_subst_tac 1,
+         atac 1,
+        hyp_subst_tac 1,
+        res_inst_tac [("n","x")] natE 1,
+         hyp_subst_tac 1,
+         atac 1,
+        hyp_subst_tac 1,
+        resolve_tac prems 1,
+        dtac spec 1,
+        etac mp 1,
+        rtac (lessI RS less_trans) 1,
+        rtac (lessI RS Suc_mono) 1]);
 
 (*** Properties of <= ***)
 
@@ -521,15 +521,15 @@
 
 goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, 
-	   dtac le_imp_less_or_eq,
-	   rtac less_or_eq_imp_le, 
-	   blast_tac (!claset addIs [less_trans])]);
+           dtac le_imp_less_or_eq,
+           rtac less_or_eq_imp_le, 
+           blast_tac (!claset addIs [less_trans])]);
 qed "le_trans";
 
 goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, 
-	   dtac le_imp_less_or_eq,
-	   blast_tac (!claset addEs [less_irrefl,less_asym])]);
+           dtac le_imp_less_or_eq,
+           blast_tac (!claset addEs [less_irrefl,less_asym])]);
 qed "le_anti_sym";
 
 goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
@@ -540,11 +540,11 @@
 
 (* Axiom 'order_le_less' of class 'order': *)
 goal thy "(m::nat) < n = (m <= n & m ~= n)";
-br iffI 1;
- br conjI 1;
-  be less_imp_le 1;
- be (less_not_refl2 RS not_sym) 1;
-by(blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
+by (rtac iffI 1);
+ by (rtac conjI 1);
+  by (etac less_imp_le 1);
+ by (etac (less_not_refl2 RS not_sym) 1);
+by (blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
 qed "nat_less_le";
 
 (** LEAST -- the least number operator **)
diff -r 7ffe67afeb94 -r 01364e2f30ad src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/RelPow.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -74,9 +74,9 @@
 by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
 by (cut_facts_tac [p1] 1);
 by (Asm_full_simp_tac 1);
-be compEpair 1;
+by (etac compEpair 1);
 by (dtac (conjI RS rel_pow_Suc_D2') 1);
-ba 1;
+by (assume_tac 1);
 by (etac exE 1);
 by (etac p3 1);
 by (etac conjunct1 1);
@@ -93,7 +93,7 @@
 by (nat_ind_tac "n" 1);
 by (blast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
 by (blast_tac (!claset addEs [rel_pow_Suc_E]
-	               addIs [rtrancl_into_rtrancl]) 1);
+                       addIs [rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";