src/Pure/pure.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12350 5fad0e7129c3
child 12723 0451211bf4a0
permissions -rw-r--r--
changed Thm.varifyT';
     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     ProofRewriteRules.setup @
    11     HTML.setup @
    12     ObjectLogic.setup @
    13     ProofContext.setup @
    14     Locale.setup @
    15     Attrib.setup @
    16     ContextRules.setup @
    17     InductAttrib.setup @
    18     Method.setup @
    19     Calculation.setup @
    20     SkipProof.setup @
    21     AxClass.setup @
    22     Latex.setup @
    23     Present.setup @
    24     Isamode.setup @
    25     ProofGeneral.setup @
    26     Codegen.setup @
    27     Goals.setup;
    28 in
    29   structure Pure =
    30   struct
    31     val thy =
    32       PureThy.begin_theory Sign.PureN [ProtoPure.thy]
    33       |> Theory.add_syntax Syntax.pure_appl_syntax
    34       |> Library.apply common_setup
    35       |> PureThy.end_theory;
    36   end;
    37 
    38   structure CPure =
    39   struct
    40     val thy =
    41       PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
    42       |> Theory.add_syntax Syntax.pure_applC_syntax
    43       |> Library.apply common_setup
    44       |> Theory.copy
    45       |> PureThy.end_theory;
    46   end;
    47 end;
    48 
    49 ThyInfo.register_theory ProtoPure.thy;
    50 ThyInfo.register_theory Pure.thy;
    51 ThyInfo.register_theory CPure.thy;