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
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 =
wenzelm@5839
    10
    Locale.setup @
wenzelm@6313
    11
    HTML.setup @
wenzelm@11761
    12
    ObjectLogic.setup @
wenzelm@5839
    13
    ProofContext.setup @
wenzelm@6770
    14
    Attrib.setup @
wenzelm@11664
    15
    InductAttrib.setup @
wenzelm@5839
    16
    Method.setup @
wenzelm@6770
    17
    Calculation.setup @
wenzelm@6888
    18
    SkipProof.setup @
berghofe@6653
    19
    AxClass.setup @
wenzelm@8965
    20
    Latex.setup @
wenzelm@7718
    21
    Present.setup @
wenzelm@6696
    22
    Isamode.setup @
berghofe@11515
    23
    ProofGeneral.setup @
berghofe@11515
    24
    Codegen.setup;
wenzelm@5839
    25
in
wenzelm@5839
    26
  structure Pure =
wenzelm@5839
    27
  struct
wenzelm@5839
    28
    val thy =
wenzelm@10931
    29
      PureThy.begin_theory Sign.PureN [ProtoPure.thy]
wenzelm@5839
    30
      |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5905
    31
      |> Library.apply common_setup
wenzelm@5839
    32
      |> PureThy.end_theory;
wenzelm@5839
    33
  end;
wenzelm@5092
    34
wenzelm@5839
    35
  structure CPure =
wenzelm@5839
    36
  struct
wenzelm@5839
    37
    val thy =
wenzelm@10931
    38
      PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
wenzelm@5839
    39
      |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5905
    40
      |> Library.apply common_setup
wenzelm@5863
    41
      |> Theory.copy
wenzelm@5839
    42
      |> PureThy.end_theory;
wenzelm@5839
    43
  end;
wenzelm@5211
    44
end;
wenzelm@5092
    45
wenzelm@6192
    46
ThyInfo.register_theory ProtoPure.thy;
wenzelm@6192
    47
ThyInfo.register_theory Pure.thy;
wenzelm@6192
    48
ThyInfo.register_theory CPure.thy;