src/HOL/TLA/ROOT.ML
author wenzelm
Tue Jul 28 17:05:34 1998 +0200 (1998-07-28)
changeset 5210 54aaa779b6b4
parent 4477 b3e5857d8d99
child 6255 db63752140c7
permissions -rw-r--r--
removed global_names flag;
     1 (*  Title:      TLA/ROOT.ML
     2 
     3 Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
     4 *)
     5 
     6 val banner = "Temporal Logic of Actions";
     7 
     8 (*
     9    raise the ambiguity level to avoid ambiguity warnings;
    10    since Trueprop and TrueInt have both empty syntax, there is
    11    an unavoidable ambiguity in the TLA (actually, Intensional) grammar.
    12 *)
    13 Syntax.ambiguity_level := 10000;
    14 
    15 (*FIXME: the old auto_tac is sometimes needed!*)
    16 fun old_auto_tac (cs,ss) = 
    17     let val cs' = cs addss ss 
    18     in  EVERY [TRY (safe_tac cs'),
    19                REPEAT (FIRSTGOAL (fast_tac cs')),
    20                TRY (safe_tac (cs addSss ss)),
    21                prune_params_tac] 
    22     end;
    23 
    24 
    25 use_thy "TLA";
    26 
    27 val TLA_build_completed = ();