src/Pure/pure.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5839 3ad1364bbb4b
child 5863 9935800edf58
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5092
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/pure.ML
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     4
5211
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
     5
Setup the actual Pure and CPure theories.
5092
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     6
*)
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
     7
5839
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
     8
local
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
     9
  val common_setup =
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    10
    ObjectLogic.setup @
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    11
    Locale.setup @
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    12
    ProofContext.setup @
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    13
    Method.setup @
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    14
    Attrib.setup;
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    15
in
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    16
  structure Pure =
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    17
  struct
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    18
    val thy =
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    19
      PureThy.begin_theory "Pure" [ProtoPure.thy]
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    20
      |> Theory.add_syntax Syntax.pure_appl_syntax
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    21
      |> Theory.apply common_setup
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    22
      |> PureThy.end_theory;
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    23
  end;
5092
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
    24
5839
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    25
  structure CPure =
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    26
  struct
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    27
    val thy =
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    28
      PureThy.begin_theory "CPure" [ProtoPure.thy]
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    29
      |> Theory.add_syntax Syntax.pure_applC_syntax
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    30
      |> Theory.apply common_setup
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    31
      |> Theory.prep_ext                  (*copy shared data!*)
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    32
      |> PureThy.end_theory;
3ad1364bbb4b Isar setups;
wenzelm
parents: 5247
diff changeset
    33
  end;
5211
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    34
end;
5092
e443bc494604 moved actual (C)Pure theories to pure.ML;
wenzelm
parents:
diff changeset
    35
5211
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    36
ThyInfo.loaded_thys :=
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    37
  (Symtab.make (map ThyInfo.mk_info
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    38
    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    39
     ("Pure", [], ["ProtoPure"], Pure.thy),
c02b0c727780 late setup of Pure and CPure;
wenzelm
parents: 5092
diff changeset
    40
     ("CPure", [], ["ProtoPure"], CPure.thy)]));