src/Pure/pure.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 14879 8989eedf72a1
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     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     Present.setup @
    23     ProofGeneral.setup @
    24     Codegen.setup @
    25     Extraction.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;