# HG changeset patch
# User paulson
# Date 913051419 -3600
# Node ID 8131f37f4ba36dfe884c4c5dc0ff1e68e62b7478
# Parent  dbb33359a7ab3c005c53da2dbf004463ca329fa1
expandshort

diff -r dbb33359a7ab -r 8131f37f4ba3 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Fri Dec 04 10:45:20 1998 +0100
+++ b/src/HOL/UNITY/Client.ML	Mon Dec 07 18:23:39 1998 +0100
@@ -131,13 +131,13 @@
 by (Clarify_tac 1);
 by (rtac Stable_transient_reachable_LeadsTo 1);
 by (res_inst_tac [("k", "k")] transient_lemma 2);
-be Disjoint_States_eq 2;
+by (etac Disjoint_States_eq 2);
 by (force_tac (claset() addDs [impOfSubs Increasing_size,
 			       impOfSubs Increasing_Stable_less],
 	       simpset()) 1);
 by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
  by (Blast_tac 1);
-be Disjoint_States_eq 1;
+by (etac Disjoint_States_eq 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
 by (ALLGOALS Force_tac);
diff -r dbb33359a7ab -r 8131f37f4ba3 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Dec 04 10:45:20 1998 +0100
+++ b/src/HOL/UNITY/Comp.ML	Mon Dec 07 18:23:39 1998 +0100
@@ -232,7 +232,7 @@
 \         (F:X --> G:X)";
 by Safe_tac;
 by (Blast_tac 1);
-auto();
+by Auto_tac;
 qed "strict_ex_refine_lemma";
 
 Goalw [strict_ex_prop_def]
@@ -249,7 +249,7 @@
 \        ALL H. States F = States H & F Join H : welldef Int X \
 \          --> G Join H : welldef |] \
 \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-bd sym 1;
+by (dtac sym 1);
 by (res_inst_tac [("x","SKIP (States G)")] allE 1
     THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,