# HG changeset patch
# User wenzelm
# Date 1205946913 -3600
# Node ID 80ec6cf82d953caf6509dfd06f34176a59e32074
# Parent  68e5eee47a45ad90ed3430e5f016edf5662b8565
removed redundant Nat.less_irrefl;

diff -r 68e5eee47a45 -r 80ec6cf82d95 src/HOL/ex/Primrec.thy
--- 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
diff -r 68e5eee47a45 -r 80ec6cf82d95 src/HOLCF/ex/Hoare.thy
--- 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)