author | wenzelm |
Sun, 17 Sep 2000 22:21:31 +0200 | |
changeset 10008 | 61eb9f3aa92a |
parent 9808 | 4e47e40c0ac5 |
child 10453 | ad91d022ab4c |
permissions | -rw-r--r-- |
3987 | 1 |
(* Title: Pure/pure_thy.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
9318 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
3987 | 5 |
|
5091 | 6 |
Theorem database, derived theory operations, and the ProtoPure theory. |
3987 | 7 |
*) |
8 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
9 |
signature BASIC_PURE_THY = |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
10 |
sig |
5000 | 11 |
val print_theorems: theory -> unit |
12 |
val print_theory: theory -> unit |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
13 |
val get_thm: theory -> xstring -> thm |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
14 |
val get_thms: theory -> xstring -> thm list |
6094 | 15 |
val get_thmss: theory -> xstring list -> thm list |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
16 |
val thms_of: theory -> (string * thm) list |
5091 | 17 |
structure ProtoPure: |
18 |
sig |
|
19 |
val thy: theory |
|
20 |
val flexpair_def: thm |
|
21 |
val Goal_def: thm |
|
22 |
end |
|
4853 | 23 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
24 |
|
3987 | 25 |
signature PURE_THY = |
26 |
sig |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
27 |
include BASIC_PURE_THY |
9808 | 28 |
val get_thm_closure: theory -> xstring -> thm |
9564 | 29 |
val get_thms_closure: theory -> xstring -> thm list |
30 |
val single_thm: string -> thm list -> thm |
|
6367 | 31 |
val cond_extern_thm_sg: Sign.sg -> string -> xstring |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
32 |
val thms_containing: theory -> string list -> (string * thm) list |
6091 | 33 |
val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm |
7405 | 34 |
val smart_store_thms: (bstring * thm list) -> thm list |
7899 | 35 |
val forall_elim_var: int -> thm -> thm |
36 |
val forall_elim_vars: int -> thm -> thm |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
37 |
val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
38 |
val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list |
9192 | 39 |
val have_thmss: theory attribute list -> ((bstring * theory attribute list) * |
40 |
(thm list * theory attribute list) list) list -> theory -> theory * (string * thm list) list |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
41 |
val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
42 |
val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
43 |
val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
44 |
val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list |
9318 | 45 |
val add_defs: bool -> ((bstring * string) * theory attribute list) list |
46 |
-> theory -> theory * thm list |
|
47 |
val add_defs_i: bool -> ((bstring * term) * theory attribute list) list |
|
48 |
-> theory -> theory * thm list |
|
49 |
val add_defss: bool -> ((bstring * string list) * theory attribute list) list |
|
50 |
-> theory -> theory * thm list list |
|
51 |
val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list |
|
52 |
-> theory -> theory * thm list list |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
53 |
val get_name: theory -> string |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
54 |
val put_name: string -> theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
55 |
val global_path: theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
56 |
val local_path: theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
57 |
val begin_theory: string -> theory list -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
58 |
val end_theory: theory -> theory |
6682 | 59 |
val checkpoint: theory -> theory |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
60 |
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory |
3987 | 61 |
end; |
62 |
||
63 |
structure PureThy: PURE_THY = |
|
64 |
struct |
|
65 |
||
66 |
||
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
67 |
(*** theorem database ***) |
3987 | 68 |
|
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
69 |
(** data kind 'Pure/theorems' **) |
3987 | 70 |
|
5005 | 71 |
structure TheoremsDataArgs = |
72 |
struct |
|
73 |
val name = "Pure/theorems"; |
|
3987 | 74 |
|
5005 | 75 |
type T = |
76 |
{space: NameSpace.T, |
|
6091 | 77 |
thms_tab: thm list Symtab.table, |
78 |
const_idx: int * (int * thm) list Symtab.table} ref; |
|
3987 | 79 |
|
4853 | 80 |
fun mk_empty _ = |
5005 | 81 |
ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T; |
3987 | 82 |
|
5005 | 83 |
val empty = mk_empty (); |
6547 | 84 |
fun copy (ref x) = ref x; |
5005 | 85 |
val prep_ext = mk_empty; |
86 |
val merge = mk_empty; |
|
87 |
||
8720 | 88 |
fun pretty sg (ref {space, thms_tab, const_idx = _}) = |
4853 | 89 |
let |
10008 | 90 |
val prt_thm = Display.pretty_thm_sg sg; |
4853 | 91 |
fun prt_thms (name, [th]) = |
92 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] |
|
93 |
| prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); |
|
3987 | 94 |
|
6846 | 95 |
val thmss = NameSpace.cond_extern_table space thms_tab; |
9215 | 96 |
in Pretty.big_list "theorems:" (map prt_thms thmss) end; |
8720 | 97 |
|
9215 | 98 |
fun print sg data = Pretty.writeln (pretty sg data); |
3987 | 99 |
end; |
100 |
||
5005 | 101 |
structure TheoremsData = TheoryDataFun(TheoremsDataArgs); |
102 |
val get_theorems_sg = TheoremsData.get_sg; |
|
103 |
val get_theorems = TheoremsData.get; |
|
104 |
||
6367 | 105 |
val cond_extern_thm_sg = NameSpace.cond_extern o #space o ! o get_theorems_sg; |
106 |
||
3987 | 107 |
|
5000 | 108 |
(* print theory *) |
3987 | 109 |
|
5005 | 110 |
val print_theorems = TheoremsData.print; |
8720 | 111 |
|
5000 | 112 |
fun print_theory thy = |
9215 | 113 |
Display.pretty_full_theory thy @ |
114 |
[TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)] |
|
8720 | 115 |
|> Pretty.chunks |> Pretty.writeln; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
116 |
|
3987 | 117 |
|
118 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
119 |
(** retrieve theorems **) |
3987 | 120 |
|
9564 | 121 |
(* selections *) |
122 |
||
123 |
fun the_thms _ (Some thms) = thms |
|
124 |
| the_thms name None = error ("Unknown theorem(s) " ^ quote name); |
|
4037 | 125 |
|
9564 | 126 |
fun single_thm _ [thm] = thm |
127 |
| single_thm name _ = error ("Single theorem expected " ^ quote name); |
|
128 |
||
129 |
||
9808 | 130 |
(* get_thm(s)_closure -- statically scoped versions *) |
9564 | 131 |
|
132 |
(*beware of proper order of evaluation!*) |
|
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
133 |
|
9564 | 134 |
fun lookup_thms thy = |
135 |
let |
|
136 |
val sg_ref = Sign.self_ref (Theory.sign_of thy); |
|
137 |
val ref {space, thms_tab, ...} = get_theorems thy; |
|
138 |
in |
|
139 |
fn name => |
|
140 |
apsome (map (Thm.transfer_sg (Sign.deref sg_ref))) (*semi-dynamic identity*) |
|
141 |
(Symtab.lookup (thms_tab, NameSpace.intern space name)) (*static content*) |
|
142 |
end; |
|
3987 | 143 |
|
9564 | 144 |
fun get_thms_closure thy = |
145 |
let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) |
|
146 |
in fn name => the_thms name (get_first (fn f => f name) closures) end; |
|
147 |
||
9808 | 148 |
fun get_thm_closure thy = |
149 |
let val get = get_thms_closure thy |
|
150 |
in fn name => single_thm name (get name) end; |
|
151 |
||
9564 | 152 |
|
153 |
(* get_thm etc. *) |
|
154 |
||
155 |
fun get_thms theory name = |
|
156 |
get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory) |
|
157 |
|> the_thms name |> map (Thm.transfer theory); |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
158 |
|
6091 | 159 |
fun get_thmss thy names = flat (map (get_thms thy) names); |
9564 | 160 |
fun get_thm thy name = single_thm name (get_thms thy name); |
4783 | 161 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
162 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
163 |
(* thms_of *) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
164 |
|
6091 | 165 |
fun attach_name thm = (Thm.name_of_thm thm, thm); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
166 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
167 |
fun thms_of thy = |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
168 |
let val ref {thms_tab, ...} = get_theorems thy in |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
169 |
map attach_name (flat (map snd (Symtab.dest thms_tab))) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
170 |
end; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
171 |
|
3987 | 172 |
|
173 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
174 |
(** theorems indexed by constants **) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
175 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
176 |
(* make index *) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
177 |
|
6091 | 178 |
fun add_const_idx ((next, table), thm) = |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
179 |
let |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
180 |
val {hyps, prop, ...} = Thm.rep_thm thm; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
181 |
val consts = |
7805
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7753
diff
changeset
|
182 |
foldr add_term_consts (hyps, add_term_consts (prop, [])); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
183 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
184 |
fun add (tab, c) = |
6091 | 185 |
Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
186 |
in (next + 1, foldl add (table, consts)) end; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
187 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
188 |
fun make_const_idx thm_tab = |
5686 | 189 |
Symtab.foldl (fn (x, (_, ths)) => foldl add_const_idx (x, ths)) ((0, Symtab.empty), thm_tab); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
190 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
191 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
192 |
(* lookup index *) |
3987 | 193 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
194 |
(*search locally*) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
195 |
fun containing [] thy = thms_of thy |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
196 |
| containing consts thy = |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
197 |
let |
4037 | 198 |
fun int ([], _) = [] |
199 |
| int (_, []) = [] |
|
200 |
| int (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) = |
|
201 |
if i = j then x :: int (xs, ys) |
|
202 |
else if i > j then int (xs, yys) |
|
203 |
else int (xxs, ys); |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
204 |
|
4037 | 205 |
fun ints [xs] = xs |
206 |
| ints xss = if exists null xss then [] else foldl int (hd xss, tl xss); |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
207 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
208 |
val ref {const_idx = (_, ctab), ...} = get_theorems thy; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
209 |
val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts; |
6977 | 210 |
in map (attach_name o snd) (ints ithmss) end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
211 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
212 |
(*search globally*) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
213 |
fun thms_containing thy consts = |
6977 | 214 |
(case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of |
7805
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7753
diff
changeset
|
215 |
[] => flat (map (containing consts) (thy :: Theory.ancestors_of thy)) |
10008 | 216 |
| cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy])) |
217 |
|> map (apsnd (Thm.transfer thy)); |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
218 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
219 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
220 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
221 |
(** store theorems **) (*DESTRUCTIVE*) |
3987 | 222 |
|
4853 | 223 |
(* naming *) |
224 |
||
225 |
fun gen_names len name = |
|
226 |
map (fn i => name ^ "_" ^ string_of_int i) (1 upto len); |
|
227 |
||
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
228 |
fun name_single name x = [(name, x)]; |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
229 |
fun name_multi name xs = gen_names (length xs) name ~~ xs; |
4853 | 230 |
|
231 |
||
6091 | 232 |
(* enter_thmx *) |
4853 | 233 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
234 |
fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
235 |
fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); |
3987 | 236 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
237 |
fun enter_thmx _ app_name ("", thmx) = map #2 (app_name "" thmx) |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
238 |
| enter_thmx sg app_name (bname, thmx) = |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
239 |
let |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
240 |
val name = Sign.full_name sg bname; |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
241 |
val named_thms = map Thm.name_thm (app_name name thmx); |
3987 | 242 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
243 |
val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
244 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
245 |
val overwrite = |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
246 |
(case Symtab.lookup (thms_tab, name) of |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
247 |
None => false |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
248 |
| Some thms' => |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
249 |
if Library.equal_lists Thm.eq_thm (thms', named_thms) then (warn_same name; false) |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
250 |
else (warn_overwrite name; true)); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
251 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
252 |
val space' = NameSpace.extend (space, [name]); |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
253 |
val thms_tab' = Symtab.update ((name, named_thms), thms_tab); |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
254 |
val const_idx' = |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
255 |
if overwrite then make_const_idx thms_tab' |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
256 |
else foldl add_const_idx (const_idx, named_thms); |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
257 |
in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; named_thms end; |
3987 | 258 |
|
4853 | 259 |
|
6091 | 260 |
(* add_thms(s) *) |
4853 | 261 |
|
6091 | 262 |
fun add_thmx app_name app_att ((bname, thmx), atts) thy = |
5280 | 263 |
let |
6091 | 264 |
val (thy', thmx') = app_att ((thy, thmx), atts); |
265 |
val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx'); |
|
266 |
in (thy', thms'') end; |
|
4853 | 267 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
268 |
fun add_thms args theory = |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
269 |
(theory, args) |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
270 |
|> foldl_map (fn (thy, arg) => add_thmx name_single Thm.apply_attributes arg thy) |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
271 |
|> apsnd (map hd); |
5907 | 272 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
273 |
fun add_thmss args theory = |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
274 |
(theory, args) |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
275 |
|> foldl_map (fn (thy, arg) => add_thmx name_multi Thm.applys_attributes arg thy); |
5907 | 276 |
|
277 |
||
6091 | 278 |
(* have_thmss *) |
5907 | 279 |
|
9192 | 280 |
local |
281 |
fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) = |
|
282 |
let |
|
283 |
fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); |
|
284 |
val (thy', thmss') = |
|
285 |
foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts @ kind_atts)) ths_atts); |
|
286 |
val thms' = flat thmss'; |
|
287 |
val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, thms'); |
|
288 |
in (thy', (bname, thms'')) end; |
|
289 |
in |
|
290 |
fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args); |
|
291 |
end; |
|
5280 | 292 |
|
293 |
||
6091 | 294 |
(* store_thm *) |
5280 | 295 |
|
6091 | 296 |
fun store_thm th_atts thy = |
297 |
let val (thy', [th']) = add_thmx name_single Thm.apply_attributes th_atts thy |
|
5280 | 298 |
in (thy', th') end; |
3987 | 299 |
|
300 |
||
7405 | 301 |
(* smart_store_thms *) |
3987 | 302 |
|
7405 | 303 |
fun smart_store_thms (name, []) = error ("Cannot store empty list of theorems: " ^ quote name) |
304 |
| smart_store_thms (name, [thm]) = enter_thmx (Thm.sign_of_thm thm) name_single (name, thm) |
|
305 |
| smart_store_thms (name, thms) = |
|
306 |
let |
|
307 |
val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm); |
|
308 |
val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms); |
|
309 |
in enter_thmx (Sign.deref sg_ref) name_multi (name, thms) end; |
|
3987 | 310 |
|
311 |
||
7899 | 312 |
(* forall_elim_vars (belongs to drule.ML) *) |
313 |
||
314 |
(*Replace outermost quantified variable by Var of given index. |
|
315 |
Could clash with Vars already present.*) |
|
316 |
fun forall_elim_var i th = |
|
317 |
let val {prop,sign,...} = rep_thm th |
|
318 |
in case prop of |
|
319 |
Const("all",_) $ Abs(a,T,_) => |
|
320 |
forall_elim (cterm_of sign (Var((a,i), T))) th |
|
321 |
| _ => raise THM("forall_elim_var", i, [th]) |
|
322 |
end; |
|
323 |
||
324 |
(*Repeat forall_elim_var until all outer quantifiers are removed*) |
|
325 |
fun forall_elim_vars i th = |
|
326 |
forall_elim_vars i (forall_elim_var i th) |
|
327 |
handle THM _ => th; |
|
328 |
||
329 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
330 |
(* store axioms as theorems *) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
331 |
|
4853 | 332 |
local |
7899 | 333 |
fun get_axs thy named_axs = |
334 |
map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs; |
|
7753 | 335 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
336 |
fun add_single add (thy, ((name, ax), atts)) = |
4853 | 337 |
let |
7753 | 338 |
val named_ax = name_single name ax; |
339 |
val thy' = add named_ax thy; |
|
340 |
val thm = hd (get_axs thy' named_ax); |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
341 |
in apsnd hd (add_thms [((name, thm), atts)] thy') end; |
7753 | 342 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
343 |
fun add_multi add (thy, ((name, axs), atts)) = |
7753 | 344 |
let |
345 |
val named_axs = name_multi name axs; |
|
4853 | 346 |
val thy' = add named_axs thy; |
7753 | 347 |
val thms = get_axs thy' named_axs; |
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
348 |
in apsnd hd (add_thmss [((name, thms), atts)] thy') end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
349 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
350 |
fun add_singles add args thy = foldl_map (add_single add) (thy, args); |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
351 |
fun add_multis add args thy = foldl_map (add_multi add) (thy, args); |
4853 | 352 |
in |
7753 | 353 |
val add_axioms = add_singles Theory.add_axioms; |
354 |
val add_axioms_i = add_singles Theory.add_axioms_i; |
|
355 |
val add_axiomss = add_multis Theory.add_axioms; |
|
356 |
val add_axiomss_i = add_multis Theory.add_axioms_i; |
|
9318 | 357 |
val add_defs = add_singles o Theory.add_defs; |
358 |
val add_defs_i = add_singles o Theory.add_defs_i; |
|
359 |
val add_defss = add_multis o Theory.add_defs; |
|
360 |
val add_defss_i = add_multis o Theory.add_defs_i; |
|
4853 | 361 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
362 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
363 |
|
3987 | 364 |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
365 |
(*** derived theory operations ***) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
366 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
367 |
(** theory management **) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
368 |
|
5005 | 369 |
(* data kind 'Pure/theory_management' *) |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
370 |
|
5005 | 371 |
structure TheoryManagementDataArgs = |
372 |
struct |
|
373 |
val name = "Pure/theory_management"; |
|
6660 | 374 |
type T = {name: string, version: int}; |
5000 | 375 |
|
6660 | 376 |
val empty = {name = "", version = 0}; |
6547 | 377 |
val copy = I; |
5005 | 378 |
val prep_ext = I; |
5000 | 379 |
fun merge _ = empty; |
5005 | 380 |
fun print _ _ = (); |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
381 |
end; |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
382 |
|
5005 | 383 |
structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs); |
384 |
val get_info = TheoryManagementData.get; |
|
385 |
val put_info = TheoryManagementData.put; |
|
386 |
||
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
387 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
388 |
(* get / put name *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
389 |
|
5000 | 390 |
val get_name = #name o get_info; |
6660 | 391 |
fun put_name name = put_info {name = name, version = 0}; |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
392 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
393 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
394 |
(* control prefixing of theory name *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
395 |
|
5210 | 396 |
val global_path = Theory.root_path; |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
397 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
398 |
fun local_path thy = |
5210 | 399 |
thy |> Theory.root_path |> Theory.add_path (get_name thy); |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
400 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
401 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
402 |
(* begin / end theory *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
403 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
404 |
fun begin_theory name thys = |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
405 |
Theory.prep_ext_merge thys |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
406 |
|> put_name name |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
407 |
|> local_path; |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
408 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
409 |
fun end_theory thy = Theory.add_name (get_name thy) thy; |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
410 |
|
6682 | 411 |
fun checkpoint thy = |
412 |
if is_draft thy then |
|
413 |
let val {name, version} = get_info thy in |
|
414 |
thy |
|
415 |
|> Theory.add_name (name ^ ":" ^ string_of_int version) |
|
416 |
|> put_info {name = name, version = version + 1} |
|
417 |
end |
|
418 |
else thy; |
|
5000 | 419 |
|
420 |
||
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
421 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
422 |
(** add logical types **) |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
423 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
424 |
fun add_typedecls decls thy = |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
425 |
let |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
426 |
val full = Sign.full_name (Theory.sign_of thy); |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
427 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
428 |
fun type_of (raw_name, vs, mx) = |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
429 |
if null (duplicates vs) then (raw_name, length vs, mx) |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
430 |
else error ("Duplicate parameters in type declaration: " ^ quote raw_name); |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
431 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
432 |
fun arity_of (raw_name, len, mx) = |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
433 |
(full (Syntax.type_name raw_name mx), replicate len logicS, logicS); |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
434 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
435 |
val types = map type_of decls; |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
436 |
val arities = map arity_of types; |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
437 |
in |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
438 |
thy |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
439 |
|> Theory.add_types types |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
440 |
|> Theory.add_arities_i arities |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
441 |
end; |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
442 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
443 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
444 |
|
5091 | 445 |
(*** the ProtoPure theory ***) |
3987 | 446 |
|
447 |
val proto_pure = |
|
448 |
Theory.pre_pure |
|
5907 | 449 |
|> Library.apply [TheoremsData.init, TheoryManagementData.init] |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
450 |
|> put_name "ProtoPure" |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
451 |
|> global_path |
3987 | 452 |
|> Theory.add_types |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
453 |
[("fun", 2, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
454 |
("prop", 0, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
455 |
("itself", 1, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
456 |
("dummy", 0, NoSyn)] |
3987 | 457 |
|> Theory.add_classes_i [(logicC, [])] |
458 |
|> Theory.add_defsort_i logicS |
|
459 |
|> Theory.add_arities_i |
|
460 |
[("fun", [logicS, logicS], logicS), |
|
461 |
("prop", [], logicS), |
|
462 |
("itself", [logicS], logicS)] |
|
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
463 |
|> Theory.add_nonterminals Syntax.pure_nonterms |
3987 | 464 |
|> Theory.add_syntax Syntax.pure_syntax |
6692 | 465 |
|> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax |
466 |
|> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax |
|
3987 | 467 |
|> Theory.add_trfuns Syntax.pure_trfuns |
468 |
|> Theory.add_trfunsT Syntax.pure_trfunsT |
|
469 |
|> Theory.add_syntax |
|
7949 | 470 |
[("==>", "[prop, prop] => prop", Delimfix "op ==>"), |
9534 | 471 |
(Term.dummy_patternN, "aprop", Delimfix "'_")] |
3987 | 472 |
|> Theory.add_consts |
473 |
[("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)), |
|
474 |
("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)), |
|
475 |
("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
|
476 |
("all", "('a => prop) => prop", Binder ("!!", 0, 0)), |
|
8039 | 477 |
("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)), |
6547 | 478 |
("TYPE", "'a itself", NoSyn), |
9534 | 479 |
(Term.dummy_patternN, "'a", Delimfix "'_")] |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
5026
diff
changeset
|
480 |
|> Theory.add_modesyntax ("", false) |
8039 | 481 |
[("Goal", "prop => prop", Mixfix ("_", [0], 0))] |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
482 |
|> local_path |
9318 | 483 |
|> (#1 oo (add_defs false o map Thm.no_attributes)) |
4788 | 484 |
[("flexpair_def", "(t =?= u) == (t == u::'a::{})"), |
485 |
("Goal_def", "GOAL (PROP A) == PROP A")] |
|
9238 | 486 |
|> (#1 o add_thmss [(("nothing", []), [])]) |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
487 |
|> end_theory; |
3987 | 488 |
|
5091 | 489 |
structure ProtoPure = |
490 |
struct |
|
491 |
val thy = proto_pure; |
|
492 |
val flexpair_def = get_axiom thy "flexpair_def"; |
|
493 |
val Goal_def = get_axiom thy "Goal_def"; |
|
494 |
end; |
|
3987 | 495 |
|
496 |
||
497 |
end; |
|
498 |
||
499 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
500 |
structure BasicPureThy: BASIC_PURE_THY = PureThy; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
501 |
open BasicPureThy; |