src/Pure/pure.ML
author wenzelm
Tue Nov 17 14:07:04 1998 +0100 (1998-11-17)
changeset 5905 68cdba6c178f
parent 5863 9935800edf58
child 6192 a42dbf1af868
permissions -rw-r--r--
Theory.apply replaced by Library.apply;
     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)]));