src/Pure/pure.ML
author wenzelm
Fri Jul 02 19:04:32 1999 +0200 (1999-07-02 ago)
changeset 6888 d0c68ebdabc5
parent 6785 10b77354862b
child 7718 86755cc5b83c
permissions -rw-r--r--
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm@5092
     1
(*  Title:      Pure/pure.ML
wenzelm@5092
     2
    ID:         $Id$
wenzelm@5092
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5092
     4
wenzelm@6192
     5
Final setup of the Pure theories.
wenzelm@5092
     6
*)
wenzelm@5092
     7
wenzelm@5839
     8
local
wenzelm@5839
     9
  val common_setup =
wenzelm@5839
    10
    Locale.setup @
wenzelm@6313
    11
    HTML.setup @
wenzelm@5839
    12
    ProofContext.setup @
wenzelm@6770
    13
    Attrib.setup @
wenzelm@5839
    14
    Method.setup @
wenzelm@6770
    15
    Calculation.setup @
wenzelm@6888
    16
    SkipProof.setup @
berghofe@6653
    17
    AxClass.setup @
wenzelm@6696
    18
    BrowserInfo.setup @
wenzelm@6696
    19
    Isamode.setup @
wenzelm@6696
    20
    ProofGeneral.setup;
wenzelm@5839
    21
in
wenzelm@5839
    22
  structure Pure =
wenzelm@5839
    23
  struct
wenzelm@5839
    24
    val thy =
wenzelm@5839
    25
      PureThy.begin_theory "Pure" [ProtoPure.thy]
wenzelm@5839
    26
      |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@5905
    27
      |> Library.apply common_setup
wenzelm@5839
    28
      |> PureThy.end_theory;
wenzelm@5839
    29
  end;
wenzelm@5092
    30
wenzelm@5839
    31
  structure CPure =
wenzelm@5839
    32
  struct
wenzelm@5839
    33
    val thy =
wenzelm@5839
    34
      PureThy.begin_theory "CPure" [ProtoPure.thy]
wenzelm@5839
    35
      |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@5905
    36
      |> Library.apply common_setup
wenzelm@5863
    37
      |> Theory.copy
wenzelm@5839
    38
      |> PureThy.end_theory;
wenzelm@5839
    39
  end;
wenzelm@5211
    40
end;
wenzelm@5092
    41
wenzelm@6192
    42
ThyInfo.register_theory ProtoPure.thy;
wenzelm@6192
    43
ThyInfo.register_theory Pure.thy;
wenzelm@6192
    44
ThyInfo.register_theory CPure.thy;