src/HOL/TLA/ROOT.ML
changeset 4477 b3e5857d8d99
parent 3945 ae9c61d69888
child 5210 54aaa779b6b4
     1.1 --- a/src/HOL/TLA/ROOT.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/ROOT.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -14,6 +14,16 @@
     1.4  
     1.5  reset global_names;
     1.6  
     1.7 +(*FIXME: the old auto_tac is sometimes needed!*)
     1.8 +fun old_auto_tac (cs,ss) = 
     1.9 +    let val cs' = cs addss ss 
    1.10 +    in  EVERY [TRY (safe_tac cs'),
    1.11 +               REPEAT (FIRSTGOAL (fast_tac cs')),
    1.12 +               TRY (safe_tac (cs addSss ss)),
    1.13 +               prune_params_tac] 
    1.14 +    end;
    1.15 +
    1.16 +
    1.17  use_thy "TLA";
    1.18  
    1.19  val TLA_build_completed = ();