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.
Merge
authorpaulson <lp15@cam.ac.uk>
Wed, 13 Jul 2016 17:20:21 +0100
changeset 63470 a911f02d8680
parent 63469 b6900858dcb9 (current diff)
parent 63468 cadd40a6cdec (diff)
child 63471 52d0adb915ee
child 63486 a4668ec480ad
Merge
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Wed Jul 13 17:14:17 2016 +0100
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Wed Jul 13 17:20:21 2016 +0100
@@ -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