Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
don't ask too much of 'transfer_prover'
authorblanchet
Mon, 28 Mar 2016 12:05:47 +0200
changeset 62733 ebfc41a47641
parent 62732 bf31fd0231ba
child 62734 38fefd98c929
don't ask too much of 'transfer_prover'
src/HOL/Corec_Examples/Tests/Small_Concrete.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -146,11 +146,16 @@
     LNil \<Rightarrow> LNil
   | LCons x r \<Rightarrow> LCons x (h3 r))"
 
-corec (friend) fold_map where
+corec fold_map where
   "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
 
+friend_of_corec fold_map where
+  "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
+   apply (rule fold_map.code)
+  sorry
 
-subsection \<open>Coinductie Natural Numbers\<close>
+
+subsection \<open>Coinductive Natural Numbers\<close>
 
 codatatype conat = CoZero | CoSuc conat
isabelle