equal
deleted
inserted
replaced
664 |
664 |
665 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; |
665 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; |
666 |
666 |
667 simpset := !simpset addcongs [ball_cong,bex_cong] |
667 simpset := !simpset addcongs [ball_cong,bex_cong] |
668 setmksimps (mksimps mksimps_pairs); |
668 setmksimps (mksimps mksimps_pairs); |
|
669 |
|
670 Addsimps[subset_UNIV, empty_subsetI, subset_refl]; |
|
671 |
|
672 |
|
673 (*** < ***) |
|
674 |
|
675 goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B"; |
|
676 by (Blast_tac 1); |
|
677 qed "psubsetI"; |
|
678 |
|
679 goalw Set.thy [psubset_def] |
|
680 "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B"; |
|
681 by (Auto_tac()); |
|
682 qed "psubset_insertD"; |