--- 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];
--- 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
--- 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];
--- 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 **)
--- 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^*";