src/Pure/pure.ML
author wenzelm
Tue Nov 17 14:07:04 1998 +0100 (1998-11-17)
changeset 5905 68cdba6c178f
parent 5863 9935800edf58
child 6192 a42dbf1af868
permissions -rw-r--r--
Theory.apply replaced by Library.apply;
wenzelm@5092
     1
(*  Title:      Pure/pure.ML
wenzelm@5092
     2
    ID:         $Id$
wenzelm@5092
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5092
     4
wenzelm@5211
     5
Setup the actual Pure and CPure theories.
wenzelm@5092
     6
*)
wenzelm@5092
     7
wenzelm@5839
     8
local
wenzelm@5839
     9
  val common_setup =
wenzelm@5839
    10
    ObjectLogic.setup @
wenzelm@5839
    11
    Locale.setup @
wenzelm@5839
    12
    ProofContext.setup @
wenzelm@5839
    13
    Method.setup @
wenzelm@5839
    14
    Attrib.setup;
wenzelm@5839
    15
in
wenzelm@5839
    16
  structure Pure =
wenzelm@5839
    17
  struct
wenzelm@5839
    18
    val thy =
wenzelm@5839
    19
      PureThy.begin_theory "Pure" [ProtoPure.thy]
wenzelm@5839
    20
      |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5905
    21
      |> Library.apply common_setup
wenzelm@5839
    22
      |> PureThy.end_theory;
wenzelm@5839
    23
  end;
wenzelm@5092
    24
wenzelm@5839
    25
  structure CPure =
wenzelm@5839
    26
  struct
wenzelm@5839
    27
    val thy =
wenzelm@5839
    28
      PureThy.begin_theory "CPure" [ProtoPure.thy]
wenzelm@5839
    29
      |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5905
    30
      |> Library.apply common_setup
wenzelm@5863
    31
      |> Theory.copy
wenzelm@5839
    32
      |> PureThy.end_theory;
wenzelm@5839
    33
  end;
wenzelm@5211
    34
end;
wenzelm@5092
    35
wenzelm@5211
    36
ThyInfo.loaded_thys :=
wenzelm@5211
    37
  (Symtab.make (map ThyInfo.mk_info
wenzelm@5211
    38
    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
wenzelm@5211
    39
     ("Pure", [], ["ProtoPure"], Pure.thy),
wenzelm@5211
    40
     ("CPure", [], ["ProtoPure"], CPure.thy)]));