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.
wenzelm@5092
     1
(*  Title:      Pure/pure.ML
wenzelm@5092
     2
    ID:         $Id$
wenzelm@5092
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5092
     4
wenzelm@6192
     5
Final setup of the Pure theories.
wenzelm@5092
     6
*)
wenzelm@5092
     7
wenzelm@5839
     8
local
wenzelm@5839
     9
  val common_setup =
berghofe@12234
    10
    ProofRewriteRules.setup @
wenzelm@6313
    11
    HTML.setup @
wenzelm@11761
    12
    ObjectLogic.setup @
wenzelm@5839
    13
    ProofContext.setup @
berghofe@12234
    14
    Locale.setup @
wenzelm@6770
    15
    Attrib.setup @
wenzelm@12350
    16
    ContextRules.setup @
wenzelm@11664
    17
    InductAttrib.setup @
wenzelm@5839
    18
    Method.setup @
wenzelm@6770
    19
    Calculation.setup @
wenzelm@6888
    20
    SkipProof.setup @
berghofe@6653
    21
    AxClass.setup @
wenzelm@7718
    22
    Present.setup @
berghofe@11515
    23
    ProofGeneral.setup @
wenzelm@12013
    24
    Codegen.setup @
berghofe@13402
    25
    Extraction.setup @
wenzelm@12013
    26
    Goals.setup;
wenzelm@5839
    27
in
wenzelm@5839
    28
  structure Pure =
wenzelm@5839
    29
  struct
wenzelm@5839
    30
    val thy =
wenzelm@10931
    31
      PureThy.begin_theory Sign.PureN [ProtoPure.thy]
wenzelm@5839
    32
      |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5905
    33
      |> Library.apply common_setup
wenzelm@5839
    34
      |> PureThy.end_theory;
wenzelm@5839
    35
  end;
wenzelm@5092
    36
wenzelm@5839
    37
  structure CPure =
wenzelm@5839
    38
  struct
wenzelm@5839
    39
    val thy =
wenzelm@10931
    40
      PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
wenzelm@5839
    41
      |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5905
    42
      |> Library.apply common_setup
wenzelm@5863
    43
      |> Theory.copy
wenzelm@5839
    44
      |> PureThy.end_theory;
wenzelm@5839
    45
  end;
wenzelm@5211
    46
end;
wenzelm@5092
    47
wenzelm@6192
    48
ThyInfo.register_theory ProtoPure.thy;
wenzelm@6192
    49
ThyInfo.register_theory Pure.thy;
wenzelm@6192
    50
ThyInfo.register_theory CPure.thy;