# HG changeset patch
# User paulson
# Date 860056197 -7200
# Node ID 62ecde1015ae8a7688dcbdb243c23992be1bdc4b
# Parent  a0fde30aa126272959db71792da562b666710261
Declares overloading for set-theoretic constants

diff -r a0fde30aa126 -r 62ecde1015ae src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Apr 03 09:46:42 1997 +0200
+++ b/src/HOL/Set.ML	Thu Apr 03 10:29:57 1997 +0200
@@ -116,6 +116,8 @@
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "subsetI";
 
+Blast.declConsts (["op <="], [subsetI]);	(*overloading of <=*)
+
 (*Rule in Modus Ponens style*)
 val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
 by (rtac (major RS bspec) 1);
@@ -165,6 +167,7 @@
 qed "subset_antisym";
 val equalityI = subset_antisym;
 
+Blast.declConsts (["op ="], [equalityI]);	(*overloading of equality*)
 AddSIs [equalityI];
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)