Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/subset.ML
changeset 9907 473a6604da94
parent 9304 342cbcb9c0d8
child 12552 d2d2ab3f1f37 
--- a/src/ZF/subset.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/subset.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -196,11 +196,11 @@
 by (blast_tac (claset() addIs prems) 1);
 qed "RepFun_subset";
 
-val subset_SIs =
+bind_thms ("subset_SIs",
     [subset_refl, cons_subsetI, subset_consI, 
      Union_least, UN_least, Un_least, 
      Inter_greatest, Int_greatest, RepFun_subset,
-     Un_upper1, Un_upper2, Int_lower1, Int_lower2];
+     Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
 
 
 (*A claset for subset reasoning*)
isabelle