src/HOL/TLA/ROOT.ML
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 3945 ae9c61d69888
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
     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 use_thy "TLA";
    16 
    17 val TLA_build_completed = ();