Ran expandshort

--- a/ex/Acc.ML	Thu Apr 06 11:35:33 1995 +0200
+++ b/ex/Acc.ML	Thu Apr 06 11:37:43 1995 +0200
@@ -33,7 +33,7 @@
 by (resolve_tac acc.intrs 1);
 by (rewtac pred_def);
 by (fast_tac set_cs 2);
-be (Int_lower1 RS Pow_mono RS subsetD) 1;
+by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
 qed "acc_induct";
 
 
@@ -46,8 +46,8 @@
 
 val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
 by (rtac (major RS wf_induct) 1);
-br (impI RS allI) 1;
-br accI 1;
+by (rtac (impI RS allI) 1);
+by (rtac accI 1);
 by (fast_tac set_cs 1);
 qed "acc_wfD_lemma";
 

--- a/ex/LList.ML	Thu Apr 06 11:35:33 1995 +0200
+++ b/ex/LList.ML	Thu Apr 06 11:37:43 1995 +0200
@@ -40,9 +40,9 @@
 
 goalw LList.thy [list_Fun_def]
     "!!M. [| M : X;  X <= list_Fun(A, X Un llist(A)) |] ==>  M : llist(A)";
-be llist.coinduct 1;
-be (subsetD RS CollectD) 1;
-ba 1;
+by (etac llist.coinduct 1);
+by (etac (subsetD RS CollectD) 1);
+by (assume_tac 1);
 qed "llist_coinduct";
 
 goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun(A,X)";
@@ -197,9 +197,9 @@
 
 goalw LList.thy [LListD_Fun_def]
     "!!M. [| M : X;  X <= LListD_Fun(r, X Un LListD(r)) |] ==>  M : LListD(r)";
-be LListD.coinduct 1;
-be (subsetD RS CollectD) 1;
-ba 1;
+by (etac LListD.coinduct 1);
+by (etac (subsetD RS CollectD) 1);
+by (assume_tac 1);
 qed "LListD_coinduct";
 
 goalw LList.thy [LListD_Fun_def,NIL_def] "<NIL,NIL> : LListD_Fun(r,s)";
@@ -223,8 +223,8 @@
 by (rtac subsetI 1);
 by (etac LListD_coinduct 1);
 by (rtac subsetI 1);
-by (eresolve_tac [diagE] 1);
-by (eresolve_tac [ssubst] 1);
+by (etac diagE 1);
+by (etac ssubst 1);
 by (eresolve_tac [llist.elim] 1);
 by (ALLGOALS
     (asm_simp_tac (llist_ss addsimps [diagI, LListD_Fun_NIL_I,
@@ -239,7 +239,7 @@
 goal LList.thy 
     "!!M N. M: llist(A) ==> <M,M> : LListD_Fun(diag(A), X Un diag(llist(A)))";
 by (rtac (LListD_eq_diag RS subst) 1);
-br LListD_Fun_LListD_I 1;
+by (rtac LListD_Fun_LListD_I 1);
 by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1);
 qed "LListD_Fun_diag_I";
 
@@ -425,14 +425,14 @@
 \                                   diag(llist(A)))		\
 \ |] ==> f(M) = g(M)";
 by (rtac LList_equalityI 1);
-br (Mlist RS imageI) 1;
+by (rtac (Mlist RS imageI) 1);
 by (rtac subsetI 1);
 by (etac imageE 1);
 by (etac ssubst 1);
 by (etac llist.elim 1);
 by (etac ssubst 1);
 by (stac NILcase 1);
-br (gMlist RS LListD_Fun_diag_I) 1;
+by (rtac (gMlist RS LListD_Fun_diag_I) 1);
 by (etac ssubst 1);
 by (REPEAT (ares_tac [CONScase] 1));
 qed "LList_fun_equalityI";
@@ -543,9 +543,9 @@
 goal LList.thy
     "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend(M,N): llist(A)";
 by (res_inst_tac [("X", "(%u.Lappend(u,N))``llist(A)")] llist_coinduct 1);
-be imageI 1;
-br subsetI 1;
-be imageE 1;
+by (etac imageI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
 by (eres_inst_tac [("a", "u")] llist.elim 1);
 by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
 by (asm_simp_tac Lappend_ss 1);
@@ -639,7 +639,7 @@
 goal LList.thy
     "prod_fun(Rep_llist, Rep_llist) `` range(%x. <x, x>) = \
 \    diag(llist(range(Leaf)))";
-br equalityI 1;
+by (rtac equalityI 1);
 by (fast_tac (univ_cs addIs [Rep_llist]) 1);
 by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
 qed "prod_fun_range_eq_diag";
@@ -677,11 +677,11 @@
 (*Utilise the "strong" part, i.e. gfp(f)*)
 goalw LList.thy [llistD_Fun_def]
      "!!l. <l,l> : llistD_Fun(r Un range(%x.<x,x>))";
-br (Rep_llist_inverse RS subst) 1;
-br prod_fun_imageI 1;
+by (rtac (Rep_llist_inverse RS subst) 1);
+by (rtac prod_fun_imageI 1);
 by (rtac (image_Un RS ssubst) 1);
 by (stac prod_fun_range_eq_diag 1);
-br (Rep_llist RS LListD_Fun_diag_I) 1;
+by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
 qed "llistD_Fun_range_I";
 
 (*A special case of list_equality for functions over lazy lists*)
@@ -754,8 +754,8 @@
 qed "lmap_iterates";
 
 goal LList.thy "iterates(f,x) = LCons(x, lmap(f, iterates(f,x)))";
-br (lmap_iterates RS ssubst) 1;
-br iterates 1;
+by (rtac (lmap_iterates RS ssubst) 1);
+by (rtac iterates 1);
 qed "iterates_lmap";
 
 (*** A rather complex proof about iterates -- cf Andy Pitts ***)
@@ -781,7 +781,7 @@
   for all u and all n::nat.*)
 val [prem] = goal LList.thy
     "(!!x. h(x) = LCons(x, lmap(f,h(x)))) ==> h = iterates(f)";
-br ext 1;
+by (rtac ext 1);
 by (res_inst_tac [("r", 
    "UN u. range(%n. <nat_rec(n, h(u), %m y.lmap(f,y)), \
 \                  nat_rec(n, iterates(f,u), %m y.lmap(f,y))>)")] 
@@ -792,12 +792,12 @@
 by (stac prem 1);
 by (stac fun_power_lmap 1);
 by (stac fun_power_lmap 1);
-br llistD_Fun_LCons_I 1;
+by (rtac llistD_Fun_LCons_I 1);
 by (rtac (lmap_iterates RS subst) 1);
 by (stac fun_power_Suc 1);
 by (stac fun_power_Suc 1);
-br (UN1_I RS UnI1) 1;
-br rangeI 1;
+by (rtac (UN1_I RS UnI1) 1);
+by (rtac rangeI 1);
 qed "iterates_equality";