src/HOL/Set.thy
changeset 26339 7825c83c9eff
parent 26150 f6bd8686b71e
child 26480 544cef16045b
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
   426 
   426 
   427 text {*
   427 text {*
   428   Gives better instantiation for bound:
   428   Gives better instantiation for bound:
   429 *}
   429 *}
   430 
   430 
   431 ML_setup {*
   431 declaration {* fn _ =>
   432   change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
   432   Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
   433 *}
   433 *}
   434 
   434 
   435 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   435 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   436   -- {* Normally the best argument order: @{prop "P x"} constrains the
   436   -- {* Normally the best argument order: @{prop "P x"} constrains the
   437     choice of @{prop "x:A"}. *}
   437     choice of @{prop "x:A"}. *}
  1029   [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
  1029   [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
  1030    ("op Int", [IntD1,IntD2]),
  1030    ("op Int", [IntD1,IntD2]),
  1031    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  1031    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  1032  *)
  1032  *)
  1033 
  1033 
  1034 ML_setup {*
  1034 ML {*
  1035   val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
  1035   val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
  1036   change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
  1036 *}
       
  1037 declaration {* fn _ =>
       
  1038   Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
  1037 *}
  1039 *}
  1038 
  1040 
  1039 
  1041 
  1040 subsubsection {* The ``proper subset'' relation *}
  1042 subsubsection {* The ``proper subset'' relation *}
  1041 
  1043