src/Pure/pure.ML
author wenzelm
Sat Nov 24 16:55:56 2001 +0100 (2001-11-24)
changeset 12284 131e743d168a
parent 12234 9d86f1cd2969
child 12301 adf0eff5ea62
permissions -rw-r--r--
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
     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     InductAttrib.setup @
    17     Method.setup @
    18     Calculation.setup @
    19     SkipProof.setup @
    20     AxClass.setup @
    21     Latex.setup @
    22     Present.setup @
    23     Isamode.setup @
    24     ProofGeneral.setup @
    25     Codegen.setup @
    26     Goals.setup;
    27 in
    28   structure Pure =
    29   struct
    30     val thy =
    31       PureThy.begin_theory Sign.PureN [ProtoPure.thy]
    32       |> Theory.add_syntax Syntax.pure_appl_syntax
    33       |> Library.apply common_setup
    34       |> PureThy.end_theory;
    35   end;
    36 
    37   structure CPure =
    38   struct
    39     val thy =
    40       PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
    41       |> Theory.add_syntax Syntax.pure_applC_syntax
    42       |> Library.apply common_setup
    43       |> Theory.copy
    44       |> PureThy.end_theory;
    45   end;
    46 end;
    47 
    48 ThyInfo.register_theory ProtoPure.thy;
    49 ThyInfo.register_theory Pure.thy;
    50 ThyInfo.register_theory CPure.thy;