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/CCL/ex/Stream.thy
changeset 59807 22bc39064290
parent 58977 9576b510f6a2
child 60754 02924903a6fd 
--- a/src/CCL/ex/Stream.thy	Wed Mar 25 10:41:53 2015 +0100
+++ b/src/CCL/ex/Stream.thy	Wed Mar 25 10:44:57 2015 +0100
@@ -120,7 +120,7 @@
 lemma iter2Blemma:
   "n:Nat \<Longrightarrow>  
     map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"
-  apply (rule_tac P = "\<lambda>x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst])
+  apply (rule_tac P = "\<lambda>x. lhs(x) = rhs" for lhs rhs in iter2B [THEN ssubst])
   apply (simp add: nmapBcons)
   done
isabelle