removed redundant Nat.less_irrefl;
authorwenzelm
Wed Mar 19 18:15:13 2008 +0100 (2008-03-19 ago)
changeset 2633480ec6cf82d95
parent 26333 68e5eee47a45
child 26335 961bbcc9d85b
removed redundant Nat.less_irrefl;
src/HOL/ex/Primrec.thy
src/HOLCF/ex/Hoare.thy
     1.1 --- a/src/HOL/ex/Primrec.thy	Wed Mar 19 18:10:23 2008 +0100
     1.2 +++ b/src/HOL/ex/Primrec.thy	Wed Mar 19 18:15:13 2008 +0100
     1.3 @@ -335,7 +335,7 @@
     1.4  lemma ack_not_PRIMREC: "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack (x, x))"
     1.5    apply (rule notI)
     1.6    apply (erule ack_bounds_PRIMREC [THEN exE])
     1.7 -  apply (rule Nat.less_irrefl)
     1.8 +  apply (rule less_irrefl [THEN notE])
     1.9    apply (drule_tac x = "[x]" in spec)
    1.10    apply simp
    1.11    done
     2.1 --- a/src/HOLCF/ex/Hoare.thy	Wed Mar 19 18:10:23 2008 +0100
     2.2 +++ b/src/HOLCF/ex/Hoare.thy	Wed Mar 19 18:15:13 2008 +0100
     2.3 @@ -84,11 +84,11 @@
     2.4  apply (intro strip)
     2.5  apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
     2.6  prefer 2 apply (assumption)
     2.7 -apply (rule le_less_trans [THEN less_irrefl])
     2.8 +apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
     2.9  prefer 2 apply (assumption)
    2.10  apply (rule Least_le)
    2.11  apply (erule hoare_lemma6)
    2.12 -apply (rule le_less_trans [THEN less_irrefl])
    2.13 +apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
    2.14  prefer 2 apply (assumption)
    2.15  apply (rule Least_le)
    2.16  apply (erule hoare_lemma7)