author | paulson |
Wed, 13 Nov 1996 10:47:08 +0100 | |
changeset 2183 | 8d42a7bccf0b |
parent 2134 | 04a71407089d |
child 2234 | 041bf27011b1 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/simpdata.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Instantiation of the generic simplifier |
|
7 |
*) |
|
8 |
||
1984 | 9 |
section "Simplifier"; |
10 |
||
923 | 11 |
open Simplifier; |
12 |
||
1922 | 13 |
(*** Integration of simplifier with classical reasoner ***) |
14 |
||
15 |
(*Add a simpset to a classical set!*) |
|
16 |
infix 4 addss; |
|
17 |
fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
|
18 |
||
19 |
fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); |
|
20 |
||
1968
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
21 |
(*Designed to be idempotent, except if best_tac instantiates variables |
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
22 |
in some of the subgoals*) |
1922 | 23 |
fun auto_tac (cs,ss) = |
24 |
ALLGOALS (asm_full_simp_tac ss) THEN |
|
1968
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
25 |
REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN |
2036 | 26 |
REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN |
27 |
prune_params_tac; |
|
1922 | 28 |
|
29 |
fun Auto_tac() = auto_tac (!claset, !simpset); |
|
30 |
||
31 |
fun auto() = by (Auto_tac()); |
|
32 |
||
33 |
||
1984 | 34 |
(*** Addition of rules to simpsets and clasets simultaneously ***) |
35 |
||
36 |
(*Takes UNCONDITIONAL theorems of the form A<->B to |
|
2031 | 37 |
the Safe Intr rule B==>A and |
38 |
the Safe Destruct rule A==>B. |
|
1984 | 39 |
Also ~A goes to the Safe Elim rule A ==> ?R |
40 |
Failing other cases, A is added as a Safe Intr rule*) |
|
41 |
local |
|
42 |
val iff_const = HOLogic.eq_const HOLogic.boolT; |
|
43 |
||
44 |
fun addIff th = |
|
45 |
(case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
|
2031 | 46 |
(Const("not",_) $ A) => |
47 |
AddSEs [zero_var_indexes (th RS notE)] |
|
48 |
| (con $ _ $ _) => |
|
49 |
if con=iff_const |
|
50 |
then (AddSIs [zero_var_indexes (th RS iffD2)]; |
|
51 |
AddSDs [zero_var_indexes (th RS iffD1)]) |
|
52 |
else AddSIs [th] |
|
53 |
| _ => AddSIs [th]; |
|
1984 | 54 |
Addsimps [th]) |
55 |
handle _ => error ("AddIffs: theorem must be unconditional\n" ^ |
|
2031 | 56 |
string_of_thm th) |
1984 | 57 |
|
58 |
fun delIff th = |
|
59 |
(case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
|
2031 | 60 |
(Const("not",_) $ A) => |
61 |
Delrules [zero_var_indexes (th RS notE)] |
|
62 |
| (con $ _ $ _) => |
|
63 |
if con=iff_const |
|
64 |
then Delrules [zero_var_indexes (th RS iffD2), |
|
65 |
zero_var_indexes (th RS iffD1)] |
|
66 |
else Delrules [th] |
|
67 |
| _ => Delrules [th]; |
|
1984 | 68 |
Delsimps [th]) |
69 |
handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ |
|
2031 | 70 |
string_of_thm th) |
1984 | 71 |
in |
72 |
val AddIffs = seq addIff |
|
73 |
val DelIffs = seq delIff |
|
74 |
end; |
|
75 |
||
76 |
||
923 | 77 |
local |
78 |
||
1922 | 79 |
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
923 | 80 |
|
1922 | 81 |
val P_imp_P_iff_True = prover "P --> (P = True)" RS mp; |
82 |
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
|
923 | 83 |
|
1922 | 84 |
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
85 |
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; |
|
923 | 86 |
|
1922 | 87 |
fun atomize pairs = |
88 |
let fun atoms th = |
|
2031 | 89 |
(case concl_of th of |
90 |
Const("Trueprop",_) $ p => |
|
91 |
(case head_of p of |
|
92 |
Const(a,_) => |
|
93 |
(case assoc(pairs,a) of |
|
94 |
Some(rls) => flat (map atoms ([th] RL rls)) |
|
95 |
| None => [th]) |
|
96 |
| _ => [th]) |
|
97 |
| _ => [th]) |
|
1922 | 98 |
in atoms end; |
923 | 99 |
|
2134 | 100 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
101 |
||
102 |
in |
|
103 |
||
1922 | 104 |
fun mk_meta_eq r = case concl_of r of |
2031 | 105 |
Const("==",_)$_$_ => r |
1922 | 106 |
| _$(Const("op =",_)$_$_) => r RS eq_reflection |
107 |
| _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False |
|
108 |
| _ => r RS P_imp_P_eq_True; |
|
109 |
(* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
|
923 | 110 |
|
2082 | 111 |
val simp_thms = map prover |
112 |
[ "(x=x) = True", |
|
113 |
"(~True) = False", "(~False) = True", "(~ ~ P) = P", |
|
114 |
"(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
|
115 |
"(True=P) = P", "(P=True) = P", |
|
116 |
"(True --> P) = P", "(False --> P) = True", |
|
117 |
"(P --> True) = True", "(P --> P) = True", |
|
118 |
"(P --> False) = (~P)", "(P --> ~P) = (~P)", |
|
119 |
"(P & True) = P", "(True & P) = P", |
|
120 |
"(P & False) = False", "(False & P) = False", "(P & P) = P", |
|
121 |
"(P | True) = True", "(True | P) = True", |
|
122 |
"(P | False) = P", "(False | P) = P", "(P | P) = P", |
|
123 |
"((~P) = (~Q)) = (P=Q)", |
|
2129 | 124 |
"(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", |
2082 | 125 |
"(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
126 |
"(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; |
|
923 | 127 |
|
988 | 128 |
(*Add congruence rules for = (instead of ==) *) |
129 |
infix 4 addcongs; |
|
923 | 130 |
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
131 |
||
1264 | 132 |
fun Addcongs congs = (simpset := !simpset addcongs congs); |
133 |
||
923 | 134 |
fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
135 |
||
1922 | 136 |
val imp_cong = impI RSN |
137 |
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
|
138 |
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); |
|
139 |
||
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
140 |
(*Miniscoping: pushing in existential quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
141 |
val ex_simps = map prover |
2031 | 142 |
["(EX x. P x & Q) = ((EX x.P x) & Q)", |
143 |
"(EX x. P & Q x) = (P & (EX x.Q x))", |
|
144 |
"(EX x. P x | Q) = ((EX x.P x) | Q)", |
|
145 |
"(EX x. P | Q x) = (P | (EX x.Q x))", |
|
146 |
"(EX x. P x --> Q) = ((ALL x.P x) --> Q)", |
|
147 |
"(EX x. P --> Q x) = (P --> (EX x.Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
148 |
|
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
149 |
(*Miniscoping: pushing in universal quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
150 |
val all_simps = map prover |
2031 | 151 |
["(ALL x. P x & Q) = ((ALL x.P x) & Q)", |
152 |
"(ALL x. P & Q x) = (P & (ALL x.Q x))", |
|
153 |
"(ALL x. P x | Q) = ((ALL x.P x) | Q)", |
|
154 |
"(ALL x. P | Q x) = (P | (ALL x.Q x))", |
|
155 |
"(ALL x. P x --> Q) = ((EX x.P x) --> Q)", |
|
156 |
"(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
157 |
|
1722 | 158 |
|
923 | 159 |
|
2022 | 160 |
(* elimination of existential quantifiers in assumptions *) |
923 | 161 |
|
162 |
val ex_all_equiv = |
|
163 |
let val lemma1 = prove_goal HOL.thy |
|
164 |
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
|
165 |
(fn prems => [resolve_tac prems 1, etac exI 1]); |
|
166 |
val lemma2 = prove_goalw HOL.thy [Ex_def] |
|
167 |
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
|
168 |
(fn prems => [REPEAT(resolve_tac prems 1)]) |
|
169 |
in equal_intr lemma1 lemma2 end; |
|
170 |
||
171 |
end; |
|
172 |
||
173 |
fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]); |
|
174 |
||
175 |
prove "conj_commute" "(P&Q) = (Q&P)"; |
|
176 |
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
177 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
2134 | 178 |
prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
923 | 179 |
|
1922 | 180 |
prove "disj_commute" "(P|Q) = (Q|P)"; |
181 |
prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; |
|
182 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
2134 | 183 |
prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))"; |
1922 | 184 |
|
923 | 185 |
prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
186 |
prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
187 |
|
1892 | 188 |
prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; |
189 |
prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; |
|
190 |
||
2134 | 191 |
prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; |
192 |
prove "imp_conjL" "((P&Q) -->R) = (P --> (Q --> R))"; |
|
193 |
prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))"; |
|
1892 | 194 |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
195 |
prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
196 |
prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
1922 | 197 |
prove "not_iff" "(P~=Q) = (P = (~Q))"; |
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
198 |
|
2134 | 199 |
(*Avoids duplication of subgoals after expand_if, when the true and false |
200 |
cases boil down to the same thing.*) |
|
201 |
prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; |
|
202 |
||
1660 | 203 |
prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))"; |
1922 | 204 |
prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; |
1660 | 205 |
prove "not_ex" "(~ (? x.P(x))) = (! x.~P(x))"; |
1922 | 206 |
prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; |
1660 | 207 |
|
1655 | 208 |
prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; |
209 |
prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
210 |
||
2134 | 211 |
(* '&' congruence rule: not included by default! |
212 |
May slow rewrite proofs down by as much as 50% *) |
|
213 |
||
214 |
let val th = prove_goal HOL.thy |
|
215 |
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
|
216 |
(fn _=> [fast_tac HOL_cs 1]) |
|
217 |
in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
218 |
||
219 |
let val th = prove_goal HOL.thy |
|
220 |
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
|
221 |
(fn _=> [fast_tac HOL_cs 1]) |
|
222 |
in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
223 |
||
224 |
(* '|' congruence rule: not included by default! *) |
|
225 |
||
226 |
let val th = prove_goal HOL.thy |
|
227 |
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
|
228 |
(fn _=> [fast_tac HOL_cs 1]) |
|
229 |
in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
|
230 |
||
231 |
prove "eq_sym_conv" "(x=y) = (y=x)"; |
|
232 |
||
233 |
qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)" |
|
234 |
(fn _ => [rtac refl 1]); |
|
235 |
||
236 |
qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y" |
|
237 |
(fn [prem] => [rewtac prem, rtac refl 1]); |
|
238 |
||
239 |
qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x" |
|
240 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
|
241 |
||
242 |
qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y" |
|
243 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
|
244 |
||
245 |
qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x" |
|
246 |
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]); |
|
247 |
(* |
|
248 |
qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y" |
|
249 |
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
|
250 |
*) |
|
251 |
qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y" |
|
252 |
(fn _ => [fast_tac (HOL_cs addIs [select_equality]) 1]); |
|
253 |
||
254 |
qed_goal "expand_if" HOL.thy |
|
255 |
"P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" |
|
256 |
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
|
257 |
stac if_P 2, |
|
258 |
stac if_not_P 1, |
|
259 |
REPEAT(fast_tac HOL_cs 1) ]); |
|
260 |
||
261 |
qed_goal "if_bool_eq" HOL.thy |
|
262 |
"(if P then Q else R) = ((P-->Q) & (~P-->R))" |
|
263 |
(fn _ => [rtac expand_if 1]); |
|
264 |
||
265 |
(** 'if' congruence rules: neither included by default! *) |
|
266 |
||
267 |
(*Simplifies x assuming c and y assuming ~c*) |
|
268 |
qed_goal "if_cong" HOL.thy |
|
269 |
"[| b=c; c ==> x=u; ~c ==> y=v |] ==>\ |
|
270 |
\ (if b then x else y) = (if c then u else v)" |
|
271 |
(fn rew::prems => |
|
272 |
[stac rew 1, stac expand_if 1, stac expand_if 1, |
|
273 |
fast_tac (HOL_cs addDs prems) 1]); |
|
274 |
||
275 |
(*Prevents simplification of x and y: much faster*) |
|
276 |
qed_goal "if_weak_cong" HOL.thy |
|
277 |
"b=c ==> (if b then x else y) = (if c then x else y)" |
|
278 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
279 |
||
280 |
(*Prevents simplification of t: much faster*) |
|
281 |
qed_goal "let_weak_cong" HOL.thy |
|
282 |
"a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
|
283 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
284 |
||
285 |
(*In general it seems wrong to add distributive laws by default: they |
|
286 |
might cause exponential blow-up. But imp_disjL has been in for a while |
|
287 |
and cannot be removed without affecting existing proofs. Moreover, |
|
288 |
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
|
289 |
grounds that it allows simplification of R in the two cases.*) |
|
290 |
||
291 |
val mksimps_pairs = |
|
292 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
293 |
("All", [spec]), ("True", []), ("False", []), |
|
294 |
("If", [if_bool_eq RS iffD1])]; |
|
1758 | 295 |
|
2082 | 296 |
val HOL_ss = empty_ss |
297 |
setmksimps (mksimps mksimps_pairs) |
|
298 |
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
|
299 |
ORELSE' etac FalseE) |
|
300 |
setsubgoaler asm_simp_tac |
|
2134 | 301 |
addsimps ([if_True, if_False, o_apply, imp_disjL, conj_assoc, disj_assoc, |
2082 | 302 |
de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] |
303 |
@ ex_simps @ all_simps @ simp_thms) |
|
304 |
addcongs [imp_cong]; |
|
305 |
||
306 |
||
2134 | 307 |
local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) |
308 |
in |
|
309 |
fun split_tac splits = mktac (map mk_meta_eq splits) |
|
310 |
end; |
|
311 |
||
312 |
local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2) |
|
313 |
in |
|
314 |
fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
|
315 |
end; |
|
316 |
||
317 |
||
1655 | 318 |
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
319 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
320 |
||
321 |
qed_goal "if_distrib" HOL.thy |
|
322 |
"f(if c then x else y) = (if c then f x else f y)" |
|
323 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
324 |
||
2097 | 325 |
qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" |
2098
2bfc0675c92f
corrected `correction` of o_assoc (of version 1.14),
oheimb
parents:
2097
diff
changeset
|
326 |
(fn _ => [rtac ext 1, rtac refl 1]); |
1984 | 327 |
|
328 |
||
329 |
||
330 |
||
331 |
(*** Install simpsets and datatypes in theory structure ***) |
|
332 |
||
333 |
simpset := HOL_ss; |
|
334 |
||
335 |
exception SS_DATA of simpset; |
|
336 |
||
337 |
let fun merge [] = SS_DATA empty_ss |
|
338 |
| merge ss = let val ss = map (fn SS_DATA x => x) ss; |
|
339 |
in SS_DATA (foldl merge_ss (hd ss, tl ss)) end; |
|
340 |
||
341 |
fun put (SS_DATA ss) = simpset := ss; |
|
342 |
||
343 |
fun get () = SS_DATA (!simpset); |
|
344 |
in add_thydata "HOL" |
|
345 |
("simpset", ThyMethods {merge = merge, put = put, get = get}) |
|
346 |
end; |
|
347 |
||
348 |
type dtype_info = {case_const:term, case_rewrites:thm list, |
|
349 |
constructors:term list, nchotomy:thm, case_cong:thm}; |
|
350 |
||
351 |
exception DT_DATA of (string * dtype_info) list; |
|
352 |
val datatypes = ref [] : (string * dtype_info) list ref; |
|
353 |
||
354 |
let fun merge [] = DT_DATA [] |
|
355 |
| merge ds = |
|
356 |
let val ds = map (fn DT_DATA x => x) ds; |
|
357 |
in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end; |
|
358 |
||
359 |
fun put (DT_DATA ds) = datatypes := ds; |
|
360 |
||
361 |
fun get () = DT_DATA (!datatypes); |
|
362 |
in add_thydata "HOL" |
|
363 |
("datatypes", ThyMethods {merge = merge, put = put, get = get}) |
|
364 |
end; |
|
365 |
||
366 |
||
367 |
add_thy_reader_file "thy_data.ML"; |