author  ballarin 
Thu, 19 Feb 2004 16:44:21 +0100  
changeset 14399  dc677b35e54f 
parent 14208  144f45277d5a 
child 14760  a08e916f4946 
permissions  rwrr 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

1 
(* Title: HOL/Hilbert_Choice.thy 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

2 
ID: $Id$ 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

4 
Copyright 2001 University of Cambridge 
12023  5 
*) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

6 

12023  7 
header {* Hilbert's epsilonoperator and everything to do with the Axiom of Choice *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

8 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

9 
theory Hilbert_Choice = NatArith 
14115  10 
files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"): 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

11 

12298  12 

13 
subsection {* Hilbert's epsilon *} 

14 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

15 
consts 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

16 
Eps :: "('a => bool) => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

17 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

18 
syntax (input) 
12298  19 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<epsilon>_./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

20 
syntax (HOL) 
12298  21 
"_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

22 
syntax 
12298  23 
"_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

24 
translations 
13764  25 
"SOME x. P" == "Eps (%x. P)" 
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

26 

f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

27 
print_translation {* 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

28 
(* to avoid etacontraction of body *) 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

29 
[("Eps", fn [Abs abs] => 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

30 
let val (x,t) = atomic_abs_tr' abs 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

31 
in Syntax.const "_Eps" $ x $ t end)] 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

32 
*} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

33 

12298  34 
axioms 
35 
someI: "P (x::'a) ==> P (SOME x. P x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

36 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

37 

12298  38 
constdefs 
39 
inv :: "('a => 'b) => ('b => 'a)" 

40 
"inv(f :: 'a => 'b) == %y. SOME x. f x = y" 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

41 

12298  42 
Inv :: "'a set => ('a => 'b) => ('b => 'a)" 
43 
"Inv A f == %x. SOME y. y : A & f y = x" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

44 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

45 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

46 
use "Hilbert_Choice_lemmas.ML" 
12372  47 
declare someI_ex [elim?]; 
48 

13585  49 
lemma Inv_mem: "[ f ` A = B; x \<in> B ] ==> Inv A f x \<in> A" 
50 
apply (unfold Inv_def) 

51 
apply (fast intro: someI2) 

52 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

53 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

54 
lemma Inv_f_eq: 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

55 
"[ inj_on f A; f x = y; x : A ] ==> Inv A f y = x" 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

56 
apply (erule subst) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

57 
apply (erule Inv_f_f) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

58 
apply assumption 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

59 
done 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

60 

dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

61 
lemma Inv_comp: 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

62 
"[ inj_on f (g ` A); inj_on g A; x : f ` g ` A ] ==> 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

63 
Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x" 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

64 
apply simp 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

65 
apply (rule Inv_f_eq) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

66 
apply (fast intro: comp_inj_on) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

67 
apply (simp add: f_Inv_f Inv_mem) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

68 
apply (simp add: Inv_mem) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

69 
done 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

70 

12298  71 
lemma tfl_some: "\<forall>P x. P x > P (Eps P)" 
72 
 {* dynamicallyscoped fact for TFL *} 

73 
by (blast intro: someI) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

74 

12298  75 

76 
subsection {* Least value operator *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

77 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

78 
constdefs 
12298  79 
LeastM :: "['a => 'b::ord, 'a => bool] => 'a" 
80 
"LeastM m P == SOME x. P x & (ALL y. P y > m x <= m y)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

81 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

82 
syntax 
12298  83 
"_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0, 4, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

84 
translations 
12298  85 
"LEAST x WRT m. P" == "LeastM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

86 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

87 
lemma LeastMI2: 
12298  88 
"P x ==> (!!y. P y ==> m x <= m y) 
89 
==> (!!x. P x ==> \<forall>y. P y > m x \<le> m y ==> Q x) 

90 
==> Q (LeastM m P)" 

91 
apply (unfold LeastM_def) 

14208  92 
apply (rule someI2_ex, blast, blast) 
12298  93 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

94 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

95 
lemma LeastM_equality: 
12298  96 
"P k ==> (!!x. P x ==> m k <= m x) 
97 
==> m (LEAST x WRT m. P x) = (m k::'a::order)" 

14208  98 
apply (rule LeastMI2, assumption, blast) 
12298  99 
apply (blast intro!: order_antisym) 
100 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

101 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

102 
lemma wf_linord_ex_has_least: 
12298  103 
"wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k 
104 
==> EX x. P x & (!y. P y > (m x,m y):r^*)" 

105 
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 

14208  106 
apply (drule_tac x = "m`Collect P" in spec, force) 
12298  107 
done 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

108 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

109 
lemma ex_has_least_nat: 
12298  110 
"P k ==> EX x. P x & (ALL y. P y > m x <= (m y::nat))" 
111 
apply (simp only: pred_nat_trancl_eq_le [symmetric]) 

112 
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 

14208  113 
apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption) 
12298  114 
done 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

115 

12298  116 
lemma LeastM_nat_lemma: 
117 
"P k ==> P (LeastM m P) & (ALL y. P y > m (LeastM m P) <= (m y::nat))" 

118 
apply (unfold LeastM_def) 

119 
apply (rule someI_ex) 

120 
apply (erule ex_has_least_nat) 

121 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

122 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

123 
lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard] 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

124 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

125 
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" 
14208  126 
by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption) 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

127 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

128 

12298  129 
subsection {* Greatest value operator *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

130 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

131 
constdefs 
12298  132 
GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" 
133 
"GreatestM m P == SOME x. P x & (ALL y. P y > m y <= m x)" 

134 

135 
Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) 

136 
"Greatest == GreatestM (%x. x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

137 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

138 
syntax 
12298  139 
"_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" 
140 
("GREATEST _ WRT _. _" [0, 4, 10] 10) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

141 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

142 
translations 
12298  143 
"GREATEST x WRT m. P" == "GreatestM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

144 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

145 
lemma GreatestMI2: 
12298  146 
"P x ==> (!!y. P y ==> m y <= m x) 
147 
==> (!!x. P x ==> \<forall>y. P y > m y \<le> m x ==> Q x) 

148 
==> Q (GreatestM m P)" 

149 
apply (unfold GreatestM_def) 

14208  150 
apply (rule someI2_ex, blast, blast) 
12298  151 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

152 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

153 
lemma GreatestM_equality: 
12298  154 
"P k ==> (!!x. P x ==> m x <= m k) 
155 
==> m (GREATEST x WRT m. P x) = (m k::'a::order)" 

14208  156 
apply (rule_tac m = m in GreatestMI2, assumption, blast) 
12298  157 
apply (blast intro!: order_antisym) 
158 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

159 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

160 
lemma Greatest_equality: 
12298  161 
"P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k" 
162 
apply (unfold Greatest_def) 

14208  163 
apply (erule GreatestM_equality, blast) 
12298  164 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

165 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

166 
lemma ex_has_greatest_nat_lemma: 
12298  167 
"P k ==> ALL x. P x > (EX y. P y & ~ ((m y::nat) <= m x)) 
168 
==> EX y. P y & ~ (m y < m k + n)" 

14208  169 
apply (induct_tac n, force) 
12298  170 
apply (force simp add: le_Suc_eq) 
171 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

172 

12298  173 
lemma ex_has_greatest_nat: 
174 
"P k ==> ALL y. P y > m y < b 

175 
==> EX x. P x & (ALL y. P y > (m y::nat) <= m x)" 

176 
apply (rule ccontr) 

177 
apply (cut_tac P = P and n = "b  m k" in ex_has_greatest_nat_lemma) 

14208  178 
apply (subgoal_tac [3] "m k <= b", auto) 
12298  179 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

180 

12298  181 
lemma GreatestM_nat_lemma: 
182 
"P k ==> ALL y. P y > m y < b 

183 
==> P (GreatestM m P) & (ALL y. P y > (m y::nat) <= m (GreatestM m P))" 

184 
apply (unfold GreatestM_def) 

185 
apply (rule someI_ex) 

14208  186 
apply (erule ex_has_greatest_nat, assumption) 
12298  187 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

188 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

189 
lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

190 

12298  191 
lemma GreatestM_nat_le: 
192 
"P x ==> ALL y. P y > m y < b 

193 
==> (m x::nat) <= m (GreatestM m P)" 

194 
apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 

195 
done 

196 

197 

198 
text {* \medskip Specialization to @{text GREATEST}. *} 

199 

200 
lemma GreatestI: "P (k::nat) ==> ALL y. P y > y < b ==> P (GREATEST x. P x)" 

201 
apply (unfold Greatest_def) 

14208  202 
apply (rule GreatestM_natI, auto) 
12298  203 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

204 

12298  205 
lemma Greatest_le: 
206 
"P x ==> ALL y. P y > y < b ==> (x::nat) <= (GREATEST x. P x)" 

207 
apply (unfold Greatest_def) 

14208  208 
apply (rule GreatestM_nat_le, auto) 
12298  209 
done 
210 

211 

212 
subsection {* The Meson proof procedure *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

213 

12298  214 
subsubsection {* Negation Normal Form *} 
215 

216 
text {* de Morgan laws *} 

217 

218 
lemma meson_not_conjD: "~(P&Q) ==> ~P  ~Q" 

219 
and meson_not_disjD: "~(PQ) ==> ~P & ~Q" 

220 
and meson_not_notD: "~~P ==> P" 

221 
and meson_not_allD: "!!P. ~(ALL x. P(x)) ==> EX x. ~P(x)" 

222 
and meson_not_exD: "!!P. ~(EX x. P(x)) ==> ALL x. ~P(x)" 

223 
by fast+ 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

224 

12298  225 
text {* Removal of @{text ">"} and @{text "<>"} (positive and 
226 
negative occurrences) *} 

227 

228 
lemma meson_imp_to_disjD: "P>Q ==> ~P  Q" 

229 
and meson_not_impD: "~(P>Q) ==> P & ~Q" 

230 
and meson_iff_to_disjD: "P=Q ==> (~P  Q) & (~Q  P)" 

231 
and meson_not_iffD: "~(P=Q) ==> (P  Q) & (~P  ~Q)" 

232 
 {* Much more efficient than @{prop "(P & ~Q)  (Q & ~P)"} for computing CNF *} 

233 
by fast+ 

234 

235 

236 
subsubsection {* Pulling out the existential quantifiers *} 

237 

238 
text {* Conjunction *} 

239 

240 
lemma meson_conj_exD1: "!!P Q. (EX x. P(x)) & Q ==> EX x. P(x) & Q" 

241 
and meson_conj_exD2: "!!P Q. P & (EX x. Q(x)) ==> EX x. P & Q(x)" 

242 
by fast+ 

243 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

244 

12298  245 
text {* Disjunction *} 
246 

247 
lemma meson_disj_exD: "!!P Q. (EX x. P(x))  (EX x. Q(x)) ==> EX x. P(x)  Q(x)" 

248 
 {* DO NOT USE with forallSkolemization: makes fewer schematic variables!! *} 

249 
 {* With exSkolemization, makes fewer Skolem constants *} 

250 
and meson_disj_exD1: "!!P Q. (EX x. P(x))  Q ==> EX x. P(x)  Q" 

251 
and meson_disj_exD2: "!!P Q. P  (EX x. Q(x)) ==> EX x. P  Q(x)" 

252 
by fast+ 

253 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

254 

12298  255 
subsubsection {* Generating clauses for the Meson Proof Procedure *} 
256 

257 
text {* Disjunctions *} 

258 

259 
lemma meson_disj_assoc: "(PQ)R ==> P(QR)" 

260 
and meson_disj_comm: "PQ ==> QP" 

261 
and meson_disj_FalseD1: "FalseP ==> P" 

262 
and meson_disj_FalseD2: "PFalse ==> P" 

263 
by fast+ 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

264 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

265 
use "meson_lemmas.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

266 
use "Tools/meson.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

267 
setup meson_setup 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

268 

14115  269 
use "Tools/specification_package.ML" 
270 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

271 
end 