src/Pure/pure.ML
author berghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998 b14e7686ce84
parent 11761 183435fd45f2
child 12013 8d2372c6b5f3
permissions -rw-r--r--
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
     1 (*  Title:      Pure/pure.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Final setup of the Pure theories.
     6 *)
     7 
     8 local
     9   val common_setup =
    10     Locale.setup @
    11     HTML.setup @
    12     ObjectLogic.setup @
    13     ProofContext.setup @
    14     Attrib.setup @
    15     InductAttrib.setup @
    16     Method.setup @
    17     Calculation.setup @
    18     SkipProof.setup @
    19     AxClass.setup @
    20     Latex.setup @
    21     Present.setup @
    22     Isamode.setup @
    23     ProofGeneral.setup @
    24     Codegen.setup;
    25 in
    26   structure Pure =
    27   struct
    28     val thy =
    29       PureThy.begin_theory Sign.PureN [ProtoPure.thy]
    30       |> Theory.add_syntax Syntax.pure_appl_syntax
    31       |> Library.apply common_setup
    32       |> PureThy.end_theory;
    33   end;
    34 
    35   structure CPure =
    36   struct
    37     val thy =
    38       PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
    39       |> Theory.add_syntax Syntax.pure_applC_syntax
    40       |> Library.apply common_setup
    41       |> Theory.copy
    42       |> PureThy.end_theory;
    43   end;
    44 end;
    45 
    46 ThyInfo.register_theory ProtoPure.thy;
    47 ThyInfo.register_theory Pure.thy;
    48 ThyInfo.register_theory CPure.thy;