# HG changeset patch
# User blanchet
# Date 1468409666 -7200
# Node ID cadd40a6cdecc5f0310c39c1a0edf79fbfb30264
# Parent  f3781c5fb03f445926406000d61ccca7cdb51d49
tuning

diff -r f3781c5fb03f -r cadd40a6cdec src/HOL/Corec_Examples/Paper_Examples.thy
--- 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)"