# HG changeset patch
# User wenzelm
# Date 935415026 -7200
# Node ID d16d7ddcc8421fca5c2f214cde6e15b224a4c95e
# Parent  b4dcc32310fbc7e9d826b8cadaa5c6be5270f0f7
isatool expandshort;

diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Hoare/Examples.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -84,7 +84,7 @@
 \ DO r := r+1 OD \
 \ {r*r <= x & x < (r+1)*(r+1)}";
 by (hoare_tac Asm_full_simp_tac 1);
-by(arith_tac 1);
+by (arith_tac 1);
 qed "sqrt";
 
 (* without multiplication *)
@@ -96,8 +96,8 @@
 \ DO r := r+1; w := w+u+2; u := u+2 OD \
 \ {r*r <= x & x < (r+1)*(r+1)}";
 by (hoare_tac Asm_full_simp_tac 1);
-by(arith_tac 1);
-by(arith_tac 1);
+by (arith_tac 1);
+by (arith_tac 1);
 qed "sqrt_without_multiplication";
 
 
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Isar_examples/Cantor.ML
--- a/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -2,14 +2,14 @@
 (* tactic script -- single steps *)
 
 Goal "EX S. S ~: range(f :: 'a => 'a set)";
-  br exI 1;
-  br notI 1;
-  be rangeE 1;
-  be equalityCE 1;
-  bd CollectD 1;
+  by (rtac exI 1);
+  by (rtac notI 1);
+  by (etac rangeE 1);
+  by (etac equalityCE 1);
+  by (dtac CollectD 1);
   by (contr_tac 1);
   by (swap_res_tac [CollectI] 1);
-  ba 1;
+  by (assume_tac 1);
 qed "it";
 
 
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/MiniML/W.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -498,7 +498,7 @@
 by (res_inst_tac [("A2","($ Sa ($ S A))")]
        ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
-by(dres_inst_tac [("s","Some ?X")] sym 1);
+by (dres_inst_tac [("s","Some ?X")] sym 1);
 by (rtac eq_free_eq_subst_scheme_list 1);
 by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -94,7 +94,7 @@
 (* transforming fun-defs into lambda-defs *)
 
 val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
- br (extensional eq) 1;
+ by (rtac (extensional eq) 1);
 qed "ext_rl";
 
 infix cc;
@@ -148,9 +148,9 @@
 (* first simplification, then model checking *)
 
 goalw Prod.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
-  br ext 1;
+  by (rtac ext 1);
   by (stac (surjective_pairing RS sym) 1);
-  br refl 1;
+  by (rtac refl 1);
 qed "pair_eta_expand";
 
 local
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -964,7 +964,7 @@
 
 (*** linearity ***)
 Goal "(x::hypreal) < y | x = y | y < x";
-by (rtac (hypreal_eq_minus_iff2 RS ssubst) 1);
+by (stac hypreal_eq_minus_iff2 1);
 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
 by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
 by (rtac hypreal_trichotomyE 1);
@@ -1083,7 +1083,7 @@
 qed "hypreal_minus_zero_less_iff2";
 
 Goal "((x::hypreal) < y) = (-y < -x)";
-by (rtac (hypreal_less_minus_iff RS ssubst) 1);
+by (stac hypreal_less_minus_iff 1);
 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
 qed "hypreal_less_swap_iff";
@@ -1103,7 +1103,7 @@
 
 Goal "(x < 0hr) = (x < -x)";
 by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
-by (rtac (hypreal_gt_zero_iff RS ssubst) 1);
+by (stac hypreal_gt_zero_iff 1);
 by (Full_simp_tac 1);
 qed "hypreal_lt_zero_iff";
 
@@ -1378,7 +1378,7 @@
 Addsimps [hypreal_two_not_zero];
 
 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
-by (rtac (hypreal_add_self RS ssubst) 1);
+by (stac hypreal_add_self 1);
 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
 qed "hypreal_sum_of_halves";
 
@@ -1495,7 +1495,7 @@
 \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
              hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
-by (rtac (hypreal_mult_assoc RS ssubst) 1);
+by (stac hypreal_mult_assoc 1);
 by (rtac (hypreal_mult_left_commute RS subst) 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
 qed "hypreal_hrinv_add";
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -190,7 +190,7 @@
                    setloop split_tac [expand_if]) 1);
 by (rewtac chain_def);
 by (rtac CollectI 1);
-by (safe_tac(claset()));
+by Safe_tac;
 by (dtac bspec 1 THEN assume_tac 1);
 by (res_inst_tac  [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2);
 by (ALLGOALS(Blast_tac));
@@ -234,7 +234,7 @@
 by (subgoal_tac "({u} Un c): super S c" 1);
 by (Asm_full_simp_tac 1);
 by (rewrite_tac [super_def,psubset_def]);
-by (safe_tac (claset()));
+by Safe_tac;
 by (fast_tac (claset() addEs [chain_extend]) 1);
 by (subgoal_tac "u ~: c" 1);
 by (blast_tac (claset() addEs [equalityE]) 1);
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Real/Real.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -715,7 +715,7 @@
 by (asm_full_simp_tac (simpset() addsimps 
 		       [real_rinv_distrib,real_add_mult_distrib,
 			real_mult_assoc RS sym]) 1);
-by (rtac (real_mult_assoc RS ssubst) 1);
+by (stac real_mult_assoc 1);
 by (rtac (real_mult_left_commute RS subst) 1);
 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
 qed "real_rinv_add";
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/W0/W.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -327,7 +327,7 @@
 (** LEVEL 80 **)
 by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
-by(dres_inst_tac [("s","Ok ?X")] sym 1);
+by (dres_inst_tac [("s","Ok ?X")] sym 1);
 by (rtac eq_free_eq_subst_tel 1);
 by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOLCF/Cont.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -671,22 +671,22 @@
 
 
 Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
-by(rtac monocontlub2cont 1);
-by( atac 1);
-by(rtac contlubI 1);
-by(strip_tac 1);
-by(forward_tac [chfin2finch] 1);
-by(rtac antisym_less 1);
-by( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
+by (rtac monocontlub2cont 1);
+by ( atac 1);
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (forward_tac [chfin2finch] 1);
+by (rtac antisym_less 1);
+by ( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
                HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);
-by(dtac (monofun_finch2finch COMP swap_prems_rl) 1);
-by( atac 1);
-by(asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1);
-by(etac conjE 1);
-by(etac exE 1);
-by(asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1);
-by(etac (monofunE RS spec RS spec RS mp) 1);
-by(etac is_ub_thelub 1);
+by (dtac (monofun_finch2finch COMP swap_prems_rl) 1);
+by ( atac 1);
+by (asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1);
+by (etac conjE 1);
+by (etac exE 1);
+by (asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1);
+by (etac (monofunE RS spec RS spec RS mp) 1);
+by (etac is_ub_thelub 1);
 qed "chfindom_monofun2cont";
 
 bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -177,14 +177,14 @@
   by (forward_tac [rewrite_rule [Impl.inv1_def]
                                 (inv1 RS invariantE) RS conjunct1] 1);
   by (tac2 1);
-  by(arith_tac 1);
+  by (arith_tac 1);
 
   (* 3 *)
   by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
 
   by (tac2 1);
   by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
-  by(arith_tac 1);
+  by (arith_tac 1);
 
   (* 2 *)
   by (tac2 1);
diff -r b4dcc32310fb -r d16d7ddcc842 src/HOLCF/IOA/Storage/Impl.ML
--- a/src/HOLCF/IOA/Storage/Impl.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOLCF/IOA/Storage/Impl.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -10,7 +10,7 @@
  "New : actions(impl_sig)       &   \
 \ Loc l : actions(impl_sig)       &   \
 \ Free l : actions(impl_sig) ";
-by(simp_tac (simpset() addsimps 
+by (simp_tac (simpset() addsimps 
              (Impl.sig_def :: actions_def :: 
               asig_projections)) 1);
 qed "in_impl_asig";