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);
     1 (*  Title:      Pure/pure.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Final setup of the Pure theories.
     6 *)
     7 
     8 local
     9   val common_setup =
    10     Locale.setup @
    11     HTML.setup @
    12     ProofContext.setup @
    13     Attrib.setup @
    14     Method.setup @
    15     Calculation.setup @
    16     SkipProof.setup @
    17     AxClass.setup @
    18     BrowserInfo.setup @
    19     Isamode.setup @
    20     ProofGeneral.setup;
    21 in
    22   structure Pure =
    23   struct
    24     val thy =
    25       PureThy.begin_theory "Pure" [ProtoPure.thy]
    26       |> Theory.add_syntax Syntax.pure_appl_syntax
    27       |> Library.apply common_setup
    28       |> PureThy.end_theory;
    29   end;
    30 
    31   structure CPure =
    32   struct
    33     val thy =
    34       PureThy.begin_theory "CPure" [ProtoPure.thy]
    35       |> Theory.add_syntax Syntax.pure_applC_syntax
    36       |> Library.apply common_setup
    37       |> Theory.copy
    38       |> PureThy.end_theory;
    39   end;
    40 end;
    41 
    42 ThyInfo.register_theory ProtoPure.thy;
    43 ThyInfo.register_theory Pure.thy;
    44 ThyInfo.register_theory CPure.thy;