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/Predicate.thy
changeset 56846 9df717fef2bb
parent 56218 1c3f1f2431f9
child 58152 6fe60a9a5bad 
--- a/src/HOL/Predicate.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Predicate.thy	Sun May 04 18:14:58 2014 +0200
@@ -498,7 +498,7 @@
   "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
 
 lemma [code]:
-  "pred_size f P = 0" by (cases P) simp
+  "size_pred f P = 0" by (cases P) simp
 
 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   "contained Empty Q \<longleftrightarrow> True"
isabelle