equal
deleted
inserted
replaced
453 apply (auto simp add: someI) |
453 apply (auto simp add: someI) |
454 done |
454 done |
455 |
455 |
456 subsection {* Subtypes (typedef), typedecl *} |
456 subsection {* Subtypes (typedef), typedecl *} |
457 |
457 |
|
458 text {* A completely unspecified non-empty subset of @{typ "'a"}: *} |
|
459 |
458 typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)" |
460 typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)" |
459 -- {* a completely unspecified non-empty subset of @{typ "'a"} *} |
|
460 by auto |
461 by auto |
461 |
462 |
462 lemma "(x::'a myTdef) = y" |
463 lemma "(x::'a myTdef) = y" |
463 refute [satsolver=dpll] |
464 refute [satsolver=dpll] |
464 oops |
465 oops |