src/Pure/pure.ML
author wenzelm
Wed Jul 29 15:38:08 1998 +0200 (1998-07-29)
changeset 5211 c02b0c727780
parent 5092 e443bc494604
child 5247 4a8e6e60bbf8
permissions -rw-r--r--
late setup of Pure and CPure;
     1 (*  Title:      Pure/pure.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Setup the actual Pure and CPure theories.
     6 *)
     7 
     8 structure Pure =
     9 struct
    10   val thy =
    11     PureThy.begin_theory "Pure" [ProtoPure.thy]
    12     |> Theory.add_syntax Syntax.pure_appl_syntax
    13     |> PureThy.end_theory;
    14 end;
    15 
    16 structure CPure =
    17 struct
    18   val thy =
    19     PureThy.begin_theory "CPure" [ProtoPure.thy]
    20     |> Theory.add_syntax Syntax.pure_applC_syntax
    21     |> PureThy.end_theory;
    22 end;
    23 
    24 ThyInfo.loaded_thys :=
    25   (Symtab.make (map ThyInfo.mk_info
    26     [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    27      ("Pure", [], ["ProtoPure"], Pure.thy),
    28      ("CPure", [], ["ProtoPure"], CPure.thy)]));