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/Hoare_Parallel/RG_Examples.thy
changeset 57512 cc97b347b301
parent 56248 67dc9549fa15
child 58884 be4d203d35b3 
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -52,7 +52,7 @@
    apply force
   apply(erule le_less_trans2) 
   apply(case_tac t,simp+)
-  apply (simp add:add_commute)
+  apply (simp add:add.commute)
   apply(simp add: add_le_mono)
 apply(rule Basic)
    apply simp
@@ -61,7 +61,7 @@
     apply simp
    apply(erule le_less_trans2)
    apply(case_tac t,simp+)
-   apply (simp add:add_commute)
+   apply (simp add:add.commute)
    apply(rule add_le_mono, auto)
 done
isabelle