src/ZF/Order.ML

     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 For Order.thy.  Orders in Zermelo-Fraenkel Set Theory 
 *)
-
-(*TO PURE/TACTIC.ML*)
-fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
 
 
 open Order;
 
 val bij_apply_cs = ZF_cs addSEs [bij_converse_bij]

 val ord_iso_apply = result();
 
 goalw Order.thy [ord_iso_def] 
     "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
 \         <converse(f) ` x, converse(f) ` y> : r";
-be CollectE 1;
-be (bspec RS bspec RS iffD2) 1;
+by (etac CollectE 1);
+by (etac (bspec RS bspec RS iffD2) 1);
 by (REPEAT (eresolve_tac [asm_rl, 
 			  bij_converse_bij RS bij_is_fun RS apply_type] 1));
 by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
 val ord_iso_converse = result();
 

 
 (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
 goal Order.thy
     "!!r. [| well_ord(A,r);  well_ord(B,s);  \
 \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
-br fun_extension 1;
-be (ord_iso_is_bij RS bij_is_fun) 1;
-be (ord_iso_is_bij RS bij_is_fun) 1;
-br well_ord_iso_unique_lemma 1;
+by (rtac fun_extension 1);
+by (etac (ord_iso_is_bij RS bij_is_fun) 1);
+by (etac (ord_iso_is_bij RS bij_is_fun) 1);
+by (rtac well_ord_iso_unique_lemma 1);
 by (REPEAT_SOME assume_tac);
 val well_ord_iso_unique = result();
 
 
 goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, 

     "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
 by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1);
 by (safe_tac ZF_cs);
 by (linear_case_tac 1);
 (*case x=xb*)
-by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1);
+by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1);
 (*case x<xb*)
 by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1);
 val well_ordI = result();
 
 goalw Order.thy [well_ord_def]

 
 (*** Derived rules for pred(A,x,r) ***)
 
 val [major,minor] = goalw Order.thy [pred_def]
     "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
-br (major RS CollectE) 1;
+by (rtac (major RS CollectE) 1);
 by (REPEAT (ares_tac [minor] 1));
 val predE = result();
 
 goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
 by (fast_tac ZF_cs 1);