moved actual (C)Pure theories to pure.ML;
authorwenzelm
Mon Jun 29 21:33:35 1998 +0200 (1998-06-29)
changeset 5092e443bc494604
parent 5091 4dc26d3e8722
child 5093 f616efb64a0e
moved actual (C)Pure theories to pure.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/goals.ML
src/Pure/pure.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Jun 29 21:33:25 1998 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Jun 29 21:33:35 1998 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
     1.5    Thy/thy_syn.ML Thy/use.ML attribute.ML axclass.ML basis.ML deriv.ML \
     1.6    display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \
     1.7 -  logic.ML net.ML pattern.ML pure_thy.ML search.ML sign.ML sorts.ML \
     1.8 +  logic.ML net.ML pattern.ML pure.ML pure_thy.ML search.ML sign.ML sorts.ML \
     1.9    tactic.ML tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML \
    1.10    type_infer.ML unify.ML
    1.11  	@./mk
     2.1 --- a/src/Pure/ROOT.ML	Mon Jun 29 21:33:25 1998 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Jun 29 21:33:35 1998 +0200
     2.3 @@ -46,6 +46,7 @@
     2.4  use "tactic.ML";
     2.5  use "goals.ML";
     2.6  use "axclass.ML";
     2.7 +use "pure.ML";
     2.8  
     2.9  (*theory parser and loader*)
    2.10  cd "Thy";
     3.1 --- a/src/Pure/goals.ML	Mon Jun 29 21:33:25 1998 +0200
     3.2 +++ b/src/Pure/goals.ML	Mon Jun 29 21:33:35 1998 +0200
     3.3 @@ -98,7 +98,7 @@
     3.4      ref((fn _=> error"No goal has been supplied in subgoal module") 
     3.5         : bool*thm->thm);
     3.6  
     3.7 -val dummy = trivial(read_cterm (sign_of Pure.thy)
     3.8 +val dummy = trivial(read_cterm (sign_of ProtoPure.thy)
     3.9      ("PROP No_goal_has_been_supplied",propT));
    3.10  
    3.11  (*List of previous goal stacks, for the undo operation.  Set by setstate. 
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/pure.ML	Mon Jun 29 21:33:35 1998 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +(*  Title:      Pure/pure.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Markus Wenzel, TU Muenchen
     4.7 +
     4.8 +The actual Pure and CPure theories.
     4.9 +*)
    4.10 +
    4.11 +structure Pure =
    4.12 +struct
    4.13 +
    4.14 +val thy =
    4.15 +  PureThy.begin_theory "Pure" [ProtoPure.thy]
    4.16 +  |> Theory.add_syntax Syntax.pure_appl_syntax
    4.17 +  |> PureThy.end_theory;
    4.18 +
    4.19 +end;
    4.20 +
    4.21 +
    4.22 +structure CPure =
    4.23 +struct
    4.24 +
    4.25 +val thy =
    4.26 +  PureThy.begin_theory "CPure" [ProtoPure.thy]
    4.27 +  |> Theory.add_syntax Syntax.pure_applC_syntax
    4.28 +  |> PureThy.end_theory;
    4.29 +
    4.30 +end;