Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HoareParallel/Gar_Coll.thy
changeset 24742 73b8b42a36b6
parent 23894 1a4167d761ac
child 26316 9e9e67e33557 
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -185,7 +185,7 @@
   apply (erule_tac x=i in allE , erule (1) notE impE)
   apply simp
   apply clarify
-  apply (drule le_imp_less_or_eq)
+  apply (drule Nat.le_imp_less_or_eq)
   apply (erule disjE)
    apply (subgoal_tac "Suc (ind x)\<le>r")
     apply fast
@@ -276,7 +276,7 @@
    apply (erule_tac x=i in allE , erule (1) notE impE)
    apply simp
    apply clarify
-   apply (drule le_imp_less_or_eq)
+   apply (drule Nat.le_imp_less_or_eq)
    apply (erule disjE)
     apply (subgoal_tac "Suc (ind x)\<le>r")
      apply fast
@@ -309,7 +309,7 @@
  apply (erule_tac x=i in allE , erule (1) notE impE)
  apply simp
  apply clarify
- apply (drule le_imp_less_or_eq)
+ apply (drule Nat.le_imp_less_or_eq)
  apply (erule disjE)
   apply (subgoal_tac "Suc (ind x)\<le>r")
    apply fast
isabelle