--- a/src/HOL/ex/Primrec.thy Wed Mar 19 18:10:23 2008 +0100
+++ b/src/HOL/ex/Primrec.thy Wed Mar 19 18:15:13 2008 +0100
@@ -335,7 +335,7 @@
lemma ack_not_PRIMREC: "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack (x, x))"
apply (rule notI)
apply (erule ack_bounds_PRIMREC [THEN exE])
- apply (rule Nat.less_irrefl)
+ apply (rule less_irrefl [THEN notE])
apply (drule_tac x = "[x]" in spec)
apply simp
done
--- a/src/HOLCF/ex/Hoare.thy Wed Mar 19 18:10:23 2008 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Mar 19 18:15:13 2008 +0100
@@ -84,11 +84,11 @@
apply (intro strip)
apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
prefer 2 apply (assumption)
-apply (rule le_less_trans [THEN less_irrefl])
+apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
prefer 2 apply (assumption)
apply (rule Least_le)
apply (erule hoare_lemma6)
-apply (rule le_less_trans [THEN less_irrefl])
+apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
prefer 2 apply (assumption)
apply (rule Least_le)
apply (erule hoare_lemma7)