# HG changeset patch
# User paulson
# Date 917626100 -3600
# Node ID be8234f37e482a217ff8820adacf2def9a28e813
# Parent  484adda70b6524b967b2b48a93025cb4b5ad82db
expandshort

diff -r 484adda70b65 -r be8234f37e48 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/Arith.ML	Fri Jan 29 17:08:20 1999 +0100
@@ -535,7 +535,7 @@
 
 Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
 by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
-be rev_mp 1;
+by (etac rev_mp 1);
 by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
 by (blast_tac (claset() addSEs [leE] 
diff -r 484adda70b65 -r be8234f37e48 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/Epsilon.ML	Fri Jan 29 17:08:20 1999 +0100
@@ -217,8 +217,8 @@
 Goal "rank(Pow(a)) = succ(rank(a))";
 by (rtac (rank RS trans) 1);
 by (rtac le_anti_sym 1);
-br UN_upper_le 2;
-br UN_least_le 1;
+by (rtac UN_upper_le 2);
+by (rtac UN_least_le 1);
 by (auto_tac (claset() addIs [rank_mono], simpset()));
 qed "rank_Pow";
 
diff -r 484adda70b65 -r be8234f37e48 src/ZF/ex/Limit.ML
--- a/src/ZF/ex/Limit.ML	Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/ex/Limit.ML	Fri Jan 29 17:08:20 1999 +0100
@@ -1425,7 +1425,7 @@
 
 Goal "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))";
 by (rtac subcpo_cpo 1);
-be subcpo_Dinf 1;
+by (etac subcpo_Dinf 1);
 by (auto_tac (claset() addIs [cpo_iprod, emb_chain_cpo], simpset()));
 qed "cpo_Dinf";
 
diff -r 484adda70b65 -r be8234f37e48 src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/ex/Primrec.ML	Fri Jan 29 17:08:20 1999 +0100
@@ -159,7 +159,7 @@
 \             i#+j < ack(succ(succ(succ(succ(k)))), j)";
 by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
 by (rtac (ack_add_bound RS lt_trans2) 2);
-br add_lt_mono 1;
+by (rtac add_lt_mono 1);
 by Auto_tac;
 qed "ack_add_bound2";
 
diff -r 484adda70b65 -r be8234f37e48 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/upair.ML	Fri Jan 29 17:08:20 1999 +0100
@@ -230,8 +230,8 @@
 by (rtac theI 1);
 by (rtac classical 1);
 by (resolve_tac prems 1);
-be (the_0 RS subst) 1;
-ba 1;
+by (etac (the_0 RS subst) 1);
+by (assume_tac 1);
 qed "theI2";
 
 (*** if -- a conditional expression for formulae ***)