src/HOL/ex/Rewrite_Examples.thy
changeset 60050 dc6ac152d864
parent 60047 58e5b16cbd94
child 60052 616a17640229
     1.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 11:58:18 2015 +0200
     1.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 12:18:47 2015 +0200
     1.3 @@ -89,15 +89,17 @@
     1.4    shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
     1.5    by (rule Orderings.order_antisym)
     1.6  
     1.7 +(* Premises of the conditional rule yield new subgoals. The
     1.8 +   assumptions of the goal are propagated into these subgoals
     1.9 +*)
    1.10  lemma
    1.11 -fixes f :: "nat \<Rightarrow> nat"
    1.12 -  assumes "f x \<le> 0" "f x \<ge> 0"
    1.13 -  shows "f x = 0"
    1.14 +  fixes f :: "nat \<Rightarrow> nat"
    1.15 +  shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
    1.16    apply (rewrite at "f x" to "0" test_theorem)
    1.17 -  apply fact
    1.18 -  apply fact
    1.19 +  apply assumption
    1.20 +  apply assumption
    1.21    apply (rule refl)
    1.22 -done
    1.23 +  done
    1.24  
    1.25  (*
    1.26     Instantiation.