equal
deleted
inserted
replaced
380 lemma test: "All (\<lambda>(x::'a list, y). x = y)" |
380 lemma test: "All (\<lambda>(x::'a list, y). x = y)" |
381 sorry |
381 sorry |
382 |
382 |
383 lemma "All (\<lambda>(x::'a fset, y). x = y)" |
383 lemma "All (\<lambda>(x::'a fset, y). x = y)" |
384 apply(lifting test) |
384 apply(lifting test) |
385 apply(cleaning) |
|
386 thm all_prs |
|
387 apply(rule all_prs) |
|
388 apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*}) |
|
389 done |
385 done |
390 |
386 |
391 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)" |
387 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)" |
392 sorry |
388 sorry |
393 |
389 |
394 lemma "Ex (\<lambda>(x::'a fset, y). x = y)" |
390 lemma "Ex (\<lambda>(x::'a fset, y). x = y)" |
395 apply(lifting test2) |
391 apply(lifting test2) |
396 apply(cleaning) |
392 done |
397 apply(rule ex_prs) |
|
398 apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*}) |
|
399 done |
|
400 |
|
401 ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *} |
|
402 |
|
403 |
|
404 |
|
405 |
393 |
406 end |
394 end |