--- a/src/ZF/quniv.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/quniv.ML Thu Sep 30 10:10:21 1993 +0100
@@ -12,12 +12,12 @@
goalw QUniv.thy [quniv_def]
"!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
-be PowI 1;
+by (etac PowI 1);
val qunivI = result();
goalw QUniv.thy [quniv_def]
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
-be PowD 1;
+by (etac PowD 1);
val qunivD = result();
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
@@ -152,8 +152,8 @@
goal Univ.thy
"!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \
\ a: Vfrom(X,i) & b: Vfrom(X,i)";
-bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;
-ba 1;
+by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
+by (assume_tac 1);
by (fast_tac ZF_cs 1);
val doubleton_in_Vfrom_D = result();
@@ -185,8 +185,8 @@
goalw QUniv.thy [QPair_def,sum_def]
"!!X. Transset(X) ==> \
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";
-br (Int_Un_distrib RS ssubst) 1;
-br Un_mono 1;
+by (rtac (Int_Un_distrib RS ssubst) 1);
+by (rtac Un_mono 1);
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
[Int_lower1, subset_refl] MRS Sigma_mono] 1));
val QPair_Int_Vfrom_succ_subset = result();
@@ -194,12 +194,12 @@
(** Pairs in quniv -- for handling the base case **)
goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";
-be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;
+by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1);
val Pair_in_quniv_D = result();
goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";
-br equalityI 1;
-br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;
+by (rtac equalityI 1);
+by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2);
by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);
val product_Int_quniv_eq = result();
@@ -211,33 +211,33 @@
(**** "Take-lemma" rules for proving c: quniv(A) ****)
goalw QUniv.thy [quniv_def] "Transset(quniv(A))";
-br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;
+by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1);
val Transset_quniv = result();
val [aprem, iprem] = goal QUniv.thy
"[| a: quniv(quniv(X)); \
\ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \
\ |] ==> a : quniv(A)";
-br (univ_Int_Vfrom_subset RS qunivI) 1;
-br (aprem RS qunivD) 1;
+by (rtac (univ_Int_Vfrom_subset RS qunivI) 1);
+by (rtac (aprem RS qunivD) 1);
by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);
-be (iprem RS qunivD) 1;
+by (etac (iprem RS qunivD) 1);
val quniv_Int_Vfrom = result();
(** Rules for level 0 **)
goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";
-br (QPair_Int_quniv_eq RS ssubst) 1;
-br (Int_lower2 RS qunivI) 1;
+by (rtac (QPair_Int_quniv_eq RS ssubst) 1);
+by (rtac (Int_lower2 RS qunivI) 1);
val QPair_Int_quniv_in_quniv = result();
(*Unused; kept as an example. QInr rule is similar*)
goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";
-br QPair_Int_quniv_in_quniv 1;
+by (rtac QPair_Int_quniv_in_quniv 1);
val QInl_Int_quniv_in_quniv = result();
goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";
-be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;
+by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1);
val Int_quniv_in_quniv = result();
goal QUniv.thy
@@ -252,8 +252,8 @@
\ b Int Vfrom(X,i) : quniv(A); \
\ Transset(X) \
\ |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";
-br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;
-br (QPair_in_quniv RS qunivD) 2;
+by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1);
+by (rtac (QPair_in_quniv RS qunivD) 2);
by (REPEAT (assume_tac 1));
val QPair_Int_Vfrom_succ_in_quniv = result();
@@ -267,7 +267,7 @@
goalw QUniv.thy [QInl_def]
"!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \
\ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";
-br QPair_Int_Vfrom_succ_in_quniv 1;
+by (rtac QPair_Int_Vfrom_succ_in_quniv 1);
by (REPEAT (ares_tac [zero_Int_in_quniv] 1));
val QInl_Int_Vfrom_succ_in_quniv = result();
@@ -276,7 +276,7 @@
goalw QUniv.thy [QPair_def]
"!!X. Transset(X) ==> \
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";
-be (Transset_Vfrom RS Transset_sum_Int_subset) 1;
+by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1);
val QPair_Int_Vfrom_subset = result();
goal QUniv.thy
@@ -284,8 +284,8 @@
\ b Int Vfrom(X,i) : quniv(A); \
\ Transset(X) \
\ |] ==> <a;b> Int Vfrom(X,i) : quniv(A)";
-br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;
-br (QPair_in_quniv RS qunivD) 2;
+by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1);
+by (rtac (QPair_in_quniv RS qunivD) 2);
by (REPEAT (assume_tac 1));
val QPair_Int_Vfrom_in_quniv = result();
@@ -309,15 +309,15 @@
"!!i. [| a Int Vset(i) <= c; \
\ b Int Vset(i) <= d \
\ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>";
-br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono]
- MRS subset_trans) 1;
+by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono]
+ MRS subset_trans) 1);
by (REPEAT (assume_tac 1));
val QPair_Int_Vset_succ_subset_trans = result();
(*Unused; kept as an example. QInr rule is similar*)
goalw QUniv.thy [QInl_def]
"!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";
-be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;
+by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1);
val QInl_Int_Vset_succ_subset_trans = result();
(*Rule for level i -- preserving the level, not decreasing it*)
@@ -325,8 +325,8 @@
"!!i. [| a Int Vset(i) <= c; \
\ b Int Vset(i) <= d \
\ |] ==> <a;b> Int Vset(i) <= <c;d>";
-br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono]
- MRS subset_trans) 1;
+by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono]
+ MRS subset_trans) 1);
by (REPEAT (assume_tac 1));
val QPair_Int_Vset_subset_trans = result();