src/Pure/pure.ML
author wenzelm
Mon Jun 29 21:33:35 1998 +0200 (1998-06-29)
changeset 5092 e443bc494604
child 5211 c02b0c727780
permissions -rw-r--r--
moved actual (C)Pure theories to pure.ML;
wenzelm@5092
     1
(*  Title:      Pure/pure.ML
wenzelm@5092
     2
    ID:         $Id$
wenzelm@5092
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5092
     4
wenzelm@5092
     5
The actual Pure and CPure theories.
wenzelm@5092
     6
*)
wenzelm@5092
     7
wenzelm@5092
     8
structure Pure =
wenzelm@5092
     9
struct
wenzelm@5092
    10
wenzelm@5092
    11
val thy =
wenzelm@5092
    12
  PureThy.begin_theory "Pure" [ProtoPure.thy]
wenzelm@5092
    13
  |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5092
    14
  |> PureThy.end_theory;
wenzelm@5092
    15
wenzelm@5092
    16
end;
wenzelm@5092
    17
wenzelm@5092
    18
wenzelm@5092
    19
structure CPure =
wenzelm@5092
    20
struct
wenzelm@5092
    21
wenzelm@5092
    22
val thy =
wenzelm@5092
    23
  PureThy.begin_theory "CPure" [ProtoPure.thy]
wenzelm@5092
    24
  |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5092
    25
  |> PureThy.end_theory;
wenzelm@5092
    26
wenzelm@5092
    27
end;