src/Pure/pure.ML
author wenzelm
Tue Aug 04 18:23:28 1998 +0200 (1998-08-04)
changeset 5247 4a8e6e60bbf8
parent 5211 c02b0c727780
child 5839 3ad1364bbb4b
permissions -rw-r--r--
Locale.setup;
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@5092
     8
structure Pure =
wenzelm@5092
     9
struct
wenzelm@5211
    10
  val thy =
wenzelm@5211
    11
    PureThy.begin_theory "Pure" [ProtoPure.thy]
wenzelm@5211
    12
    |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5247
    13
    |> Theory.apply Locale.setup
wenzelm@5211
    14
    |> PureThy.end_theory;
wenzelm@5092
    15
end;
wenzelm@5092
    16
wenzelm@5092
    17
structure CPure =
wenzelm@5092
    18
struct
wenzelm@5211
    19
  val thy =
wenzelm@5211
    20
    PureThy.begin_theory "CPure" [ProtoPure.thy]
wenzelm@5211
    21
    |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5247
    22
    |> Theory.apply Locale.setup
wenzelm@5211
    23
    |> PureThy.end_theory;
wenzelm@5211
    24
end;
wenzelm@5092
    25
wenzelm@5211
    26
ThyInfo.loaded_thys :=
wenzelm@5211
    27
  (Symtab.make (map ThyInfo.mk_info
wenzelm@5211
    28
    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
wenzelm@5211
    29
     ("Pure", [], ["ProtoPure"], Pure.thy),
wenzelm@5211
    30
     ("CPure", [], ["ProtoPure"], CPure.thy)]));