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;
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
wenzelm@3807
    15
use_thy "TLA";
wenzelm@3807
    16
wenzelm@3807
    17
val TLA_build_completed = ();