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;
wenzelm@3807
     1
(*  Title:      TLA/ROOT.ML
wenzelm@3807
     2
wenzelm@3807
     3
Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
wenzelm@3807
     4
*)
wenzelm@3807
     5
wenzelm@3807
     6
val banner = "Temporal Logic of Actions";
wenzelm@3807
     7
wenzelm@3807
     8
(*
wenzelm@3807
     9
   raise the ambiguity level to avoid ambiguity warnings;
wenzelm@3807
    10
   since Trueprop and TrueInt have both empty syntax, there is
wenzelm@3807
    11
   an unavoidable ambiguity in the TLA (actually, Intensional) grammar.
wenzelm@3807
    12
*)
wenzelm@3807
    13
Syntax.ambiguity_level := 10000;
wenzelm@3807
    14
paulson@4477
    15
(*FIXME: the old auto_tac is sometimes needed!*)
paulson@4477
    16
fun old_auto_tac (cs,ss) = 
paulson@4477
    17
    let val cs' = cs addss ss 
paulson@4477
    18
    in  EVERY [TRY (safe_tac cs'),
paulson@4477
    19
               REPEAT (FIRSTGOAL (fast_tac cs')),
paulson@4477
    20
               TRY (safe_tac (cs addSss ss)),
paulson@4477
    21
               prune_params_tac] 
paulson@4477
    22
    end;
paulson@4477
    23
paulson@4477
    24
wenzelm@3807
    25
use_thy "TLA";
wenzelm@3807
    26
wenzelm@3807
    27
val TLA_build_completed = ();