src/Pure/pure.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5905 68cdba6c178f
child 6192 a42dbf1af868
permissions -rw-r--r--
tidying
     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       |> Library.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       |> Library.apply common_setup
    31       |> Theory.copy
    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)]));