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.
tuning
authorblanchet
Wed, 13 Jul 2016 13:34:26 +0200
changeset 63468 cadd40a6cdec
parent 63467 f3781c5fb03f
child 63470 a911f02d8680
tuning
src/HOL/Corec_Examples/Paper_Examples.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Wed Jul 13 13:34:26 2016 +0200
@@ -20,7 +20,7 @@
   "natsFrom n = n \<lhd> natsFrom (n + 1)"
 
 corec (friend) add1 :: "nat stream \<Rightarrow> nat stream"
-where "add1 n = (shd n + 1) \<lhd> add1 (stl n)"
+where "add1 ns = (shd ns + 1) \<lhd> add1 (stl ns)"
 
 corec natsFrom' :: "nat \<Rightarrow> nat stream" where
   "natsFrom' n = n \<lhd> add1 (natsFrom' n)"
isabelle