--- a/src/HOL/HOL.thy Sat Sep 19 22:32:26 2015 +0200
+++ b/src/HOL/HOL.thy Mon Sep 21 11:31:56 2015 +0200
@@ -1691,6 +1691,32 @@
\<close>
+text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+not to simplify the argument and to solve it by an assumption. *}
+
+definition ASSUMPTION :: "bool \<Rightarrow> bool" where
+"ASSUMPTION A \<equiv> A"
+
+lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
+by (rule refl)
+
+lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
+by(simp add: ASSUMPTION_def)
+
+lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
+by(simp add: ASSUMPTION_def)
+
+setup {*
+let
+ val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
+ resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
+ resolve_tac ctxt (Simplifier.prems_of ctxt))
+in
+ map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
+end
+*}
+
+
subsection \<open>Code generator setup\<close>
subsubsection \<open>Generic code generator preprocessor setup\<close>