isabelle: src/HOL/AxClasses/Lattice/tools.ML@82a5ca6290aa (annotated)

1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	1
de6f18da81bb added this stuff; wenzelm parents: diff changeset	2	( generic tools )
de6f18da81bb added this stuff; wenzelm parents: diff changeset	3
de6f18da81bb added this stuff; wenzelm parents: diff changeset	4	val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)";
de6f18da81bb added this stuff; wenzelm parents: diff changeset	5	by (resolve_tac prems 1);
de6f18da81bb added this stuff; wenzelm parents: diff changeset	6	qed "selectI1";
de6f18da81bb added this stuff; wenzelm parents: diff changeset	7
de6f18da81bb added this stuff; wenzelm parents: diff changeset	8	goal HOL.thy "(P & Q) = (Q & P)";
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	9	by (Fast_tac 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	10	qed "conj_commut";