--- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 11:58:18 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 12:18:47 2015 +0200
@@ -89,15 +89,17 @@
shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
by (rule Orderings.order_antisym)
+(* Premises of the conditional rule yield new subgoals. The
+ assumptions of the goal are propagated into these subgoals
+*)
lemma
-fixes f :: "nat \<Rightarrow> nat"
- assumes "f x \<le> 0" "f x \<ge> 0"
- shows "f x = 0"
+ fixes f :: "nat \<Rightarrow> nat"
+ shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
apply (rewrite at "f x" to "0" test_theorem)
- apply fact
- apply fact
+ apply assumption
+ apply assumption
apply (rule refl)
-done
+ done
(*
Instantiation.