src/Pure/pure.ML
author wenzelm
Mon Nov 09 15:41:24 1998 +0100 (1998-11-09)
changeset 5839 3ad1364bbb4b
parent 5247 4a8e6e60bbf8
child 5863 9935800edf58
permissions -rw-r--r--
Isar setups;
     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 local
     9   val common_setup =
    10     ObjectLogic.setup @
    11     Locale.setup @
    12     ProofContext.setup @
    13     Method.setup @
    14     Attrib.setup;
    15 in
    16   structure Pure =
    17   struct
    18     val thy =
    19       PureThy.begin_theory "Pure" [ProtoPure.thy]
    20       |> Theory.add_syntax Syntax.pure_appl_syntax
    21       |> Theory.apply common_setup
    22       |> PureThy.end_theory;
    23   end;
    24 
    25   structure CPure =
    26   struct
    27     val thy =
    28       PureThy.begin_theory "CPure" [ProtoPure.thy]
    29       |> Theory.add_syntax Syntax.pure_applC_syntax
    30       |> Theory.apply common_setup
    31       |> Theory.prep_ext                  (*copy shared data!*)
    32       |> PureThy.end_theory;
    33   end;
    34 end;
    35 
    36 ThyInfo.loaded_thys :=
    37   (Symtab.make (map ThyInfo.mk_info
    38     [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    39      ("Pure", [], ["ProtoPure"], Pure.thy),
    40      ("CPure", [], ["ProtoPure"], CPure.thy)]));