equal
deleted
inserted
replaced
413 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*) |
413 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*) |
414 AddSIs [singletonI]; |
414 AddSIs [singletonI]; |
415 |
415 |
416 AddSDs [singleton_inject]; |
416 AddSDs [singleton_inject]; |
417 |
417 |
|
418 goal Set.thy "{x.x=a} = {a}"; |
|
419 by(Blast_tac 1); |
|
420 qed "singleton_conv"; |
|
421 Addsimps [singleton_conv]; |
418 |
422 |
419 section "The universal set -- UNIV"; |
423 section "The universal set -- UNIV"; |
420 |
424 |
421 qed_goal "UNIV_I" Set.thy "x : UNIV" |
425 qed_goal "UNIV_I" Set.thy "x : UNIV" |
422 (fn _ => [rtac ComplI 1, etac emptyE 1]); |
426 (fn _ => [rtac ComplI 1, etac emptyE 1]); |