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/Proofs/Lambda/ListApplication.thy
changeset 67399 eab6ce8368fa
parent 66311 037aaa0b6daf 
--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -9,7 +9,7 @@
 
 abbreviation
   list_application :: "dB => dB list => dB"  (infixl "\<degree>\<degree>" 150) where
-  "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
+  "t \<degree>\<degree> ts == foldl (\<degree>) t ts"
 
 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
   by (induct ts rule: rev_induct) auto
@@ -75,7 +75,7 @@
   done
 
 lemma size_apps [simp]:
-  "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
+  "size (r \<degree>\<degree> rs) = size r + foldl (+) 0 (map size rs) + length rs"
   by (induct rs rule: rev_induct) auto
 
 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
isabelle