src/Pure/pure.ML
author wenzelm
Tue Aug 04 18:23:28 1998 +0200 (1998-08-04)
changeset 5247 4a8e6e60bbf8
parent 5211 c02b0c727780
child 5839 3ad1364bbb4b
permissions -rw-r--r--
Locale.setup;
     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     |> Theory.apply Locale.setup
    14     |> PureThy.end_theory;
    15 end;
    16 
    17 structure CPure =
    18 struct
    19   val thy =
    20     PureThy.begin_theory "CPure" [ProtoPure.thy]
    21     |> Theory.add_syntax Syntax.pure_applC_syntax
    22     |> Theory.apply Locale.setup
    23     |> PureThy.end_theory;
    24 end;
    25 
    26 ThyInfo.loaded_thys :=
    27   (Symtab.make (map ThyInfo.mk_info
    28     [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    29      ("Pure", [], ["ProtoPure"], Pure.thy),
    30      ("CPure", [], ["ProtoPure"], CPure.thy)]));