equal
deleted
inserted
replaced
214 (* effect on printed locale *) |
214 (* effect on printed locale *) |
215 |
215 |
216 print_locale! rgrp |
216 print_locale! rgrp |
217 print_locale! lgrp |
217 print_locale! lgrp |
218 |
218 |
219 end |
219 |
|
220 (* locale with many parameters --- |
|
221 interpretations generate alternating group A5 *) |
|
222 |
|
223 locale A5 = |
|
224 fixes A and B and C and D and E |
|
225 assumes eq: "A <-> B <-> C <-> D <-> E" |
|
226 |
|
227 sublocale A5 < 1: A5 _ _ D E C |
|
228 print_facts |
|
229 using eq apply (blast intro: A5.intro) done |
|
230 |
|
231 sublocale A5 < 2: A5 C _ E _ A |
|
232 print_facts |
|
233 using eq apply (blast intro: A5.intro) done |
|
234 |
|
235 sublocale A5 < 3: A5 B C A _ _ |
|
236 print_facts |
|
237 using eq apply (blast intro: A5.intro) done |
|
238 |
|
239 (* Any even permutation of parameters is subsumed by the above. *) |
|
240 |
|
241 print_locale! A5 |
|
242 |
|
243 |
|
244 (* Free arguments of instance *) |
|
245 |
|
246 locale trivial = |
|
247 fixes P and Q :: o |
|
248 assumes Q: "P <-> P <-> Q" |
|
249 begin |
|
250 |
|
251 lemma Q_triv: "Q" using Q by fast |
|
252 |
|
253 end |
|
254 |
|
255 sublocale trivial < x: trivial x _ |
|
256 apply (intro trivial.intro) using Q by fast |
|
257 |
|
258 print_locale! trivial |
|
259 |
|
260 context trivial begin thm x.Q [where ?x = True] end |
|
261 |
|
262 end |