expandshort
authorpaulson
Mon Dec 07 18:23:39 1998 +0100 (1998-12-07)
changeset 60188131f37f4ba3
parent 6017 dbb33359a7ab
child 6019 0e55c2fb2ebb
expandshort
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Comp.ML
     1.1 --- a/src/HOL/UNITY/Client.ML	Fri Dec 04 10:45:20 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Client.ML	Mon Dec 07 18:23:39 1998 +0100
     1.3 @@ -131,13 +131,13 @@
     1.4  by (Clarify_tac 1);
     1.5  by (rtac Stable_transient_reachable_LeadsTo 1);
     1.6  by (res_inst_tac [("k", "k")] transient_lemma 2);
     1.7 -be Disjoint_States_eq 2;
     1.8 +by (etac Disjoint_States_eq 2);
     1.9  by (force_tac (claset() addDs [impOfSubs Increasing_size,
    1.10  			       impOfSubs Increasing_Stable_less],
    1.11  	       simpset()) 1);
    1.12  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    1.13   by (Blast_tac 1);
    1.14 -be Disjoint_States_eq 1;
    1.15 +by (etac Disjoint_States_eq 1);
    1.16  by (auto_tac (claset(),
    1.17  	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
    1.18  by (ALLGOALS Force_tac);
     2.1 --- a/src/HOL/UNITY/Comp.ML	Fri Dec 04 10:45:20 1998 +0100
     2.2 +++ b/src/HOL/UNITY/Comp.ML	Mon Dec 07 18:23:39 1998 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4  \         (F:X --> G:X)";
     2.5  by Safe_tac;
     2.6  by (Blast_tac 1);
     2.7 -auto();
     2.8 +by Auto_tac;
     2.9  qed "strict_ex_refine_lemma";
    2.10  
    2.11  Goalw [strict_ex_prop_def]
    2.12 @@ -249,7 +249,7 @@
    2.13  \        ALL H. States F = States H & F Join H : welldef Int X \
    2.14  \          --> G Join H : welldef |] \
    2.15  \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
    2.16 -bd sym 1;
    2.17 +by (dtac sym 1);
    2.18  by (res_inst_tac [("x","SKIP (States G)")] allE 1
    2.19      THEN assume_tac 1);
    2.20  by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,