src/HOL/TLA/TLA.ML
changeset 4423 a129b817b58a
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/TLA/TLA.ML	Tue Dec 16 15:17:26 1997 +0100
     1.2 +++ b/src/HOL/TLA/TLA.ML	Tue Dec 16 17:58:03 1997 +0100
     1.3 @@ -1046,12 +1046,12 @@
     1.4     example of a history variable: existence of a clock
     1.5  
     1.6  goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))";
     1.7 -br tempI 1;
     1.8 -br historyI 1;
     1.9 -bws action_rews;
    1.10 +by (rtac tempI 1);
    1.11 +by (rtac historyI 1);
    1.12 +by (rewrite_goals_tac action_rews);
    1.13  by (TRYALL (rtac impI));
    1.14  by (TRYALL (etac conjE));
    1.15 -ba 3;
    1.16 +by (assume_tac 3);
    1.17  by (Asm_full_simp_tac 3);
    1.18  by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
    1.19  (** solved **)