src/HOL/Hyperreal/Integration.ML

--- a/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:25:40 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:26:27 2004 +0200
@@ -10,6 +10,13 @@
 fun ARITH_PROVE str = prove_goal thy str
                       (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
 
+fun CLAIM_SIMP str thms =
+               prove_goal (the_context()) str
+               (fn prems => [cut_facts_tac prems 1,
+                   auto_tac (claset(),simpset() addsimps thms)]);
+
+fun CLAIM str = CLAIM_SIMP str [];
+
 Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
 by Auto_tac;
 qed "partition_zero";