Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added an important default rule
authorpaulson
Thu, 13 Jul 2000 13:04:48 +0200
changeset 9304 342cbcb9c0d8
parent 9303 f1ad1ed0d110
child 9305 3dfae8f90dcf
added an important default rule
src/ZF/subset.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/subset.ML	Thu Jul 13 13:02:20 2000 +0200
+++ b/src/ZF/subset.ML	Thu Jul 13 13:04:48 2000 +0200
@@ -20,6 +20,7 @@
 Goal "cons(a,B)<=C <-> a:C & B<=C";
 by (Blast_tac 1);
 qed "cons_subset_iff";
+AddIffs [cons_subset_iff];
 
 (*A safe special case of subset elimination, adding no new variables 
   [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
isabelle