src/Pure/pure.ML
author wenzelm
Thu, 01 Nov 2001 21:10:13 +0100
changeset 12013 8d2372c6b5f3
parent 11761 183435fd45f2
child 12234 9d86f1cd2969
permissions -rw-r--r--
Goals.setup;

(*  Title:      Pure/pure.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Final setup of the Pure theories.
*)

local
  val common_setup =
    Locale.setup @
    HTML.setup @
    ObjectLogic.setup @
    ProofContext.setup @
    Attrib.setup @
    InductAttrib.setup @
    Method.setup @
    Calculation.setup @
    SkipProof.setup @
    AxClass.setup @
    Latex.setup @
    Present.setup @
    Isamode.setup @
    ProofGeneral.setup @
    Codegen.setup @
    Goals.setup;
in
  structure Pure =
  struct
    val thy =
      PureThy.begin_theory Sign.PureN [ProtoPure.thy]
      |> Theory.add_syntax Syntax.pure_appl_syntax
      |> Library.apply common_setup
      |> PureThy.end_theory;
  end;

  structure CPure =
  struct
    val thy =
      PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
      |> Theory.add_syntax Syntax.pure_applC_syntax
      |> Library.apply common_setup
      |> Theory.copy
      |> PureThy.end_theory;
  end;
end;

ThyInfo.register_theory ProtoPure.thy;
ThyInfo.register_theory Pure.thy;
ThyInfo.register_theory CPure.thy;