src/HOL/TLA/ROOT.ML
changeset 6255 db63752140c7
parent 5210 54aaa779b6b4
child 6349 f7750d816c21
     1.1 --- a/src/HOL/TLA/ROOT.ML	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/ROOT.ML	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -5,23 +5,6 @@
     1.4  
     1.5  val banner = "Temporal Logic of Actions";
     1.6  
     1.7 -(*
     1.8 -   raise the ambiguity level to avoid ambiguity warnings;
     1.9 -   since Trueprop and TrueInt have both empty syntax, there is
    1.10 -   an unavoidable ambiguity in the TLA (actually, Intensional) grammar.
    1.11 -*)
    1.12 -Syntax.ambiguity_level := 10000;
    1.13 -
    1.14 -(*FIXME: the old auto_tac is sometimes needed!*)
    1.15 -fun old_auto_tac (cs,ss) = 
    1.16 -    let val cs' = cs addss ss 
    1.17 -    in  EVERY [TRY (safe_tac cs'),
    1.18 -               REPEAT (FIRSTGOAL (fast_tac cs')),
    1.19 -               TRY (safe_tac (cs addSss ss)),
    1.20 -               prune_params_tac] 
    1.21 -    end;
    1.22 -
    1.23 -
    1.24  use_thy "TLA";
    1.25  
    1.26  val TLA_build_completed = ();