my forest
fix bug
+1
-1
+1
-1
trees/isa/isa-001T.tree
+1
-1
trees/isa/isa-001T.tree
···
7
7
\parent{isa-001B}
8
8
\shiki{definition twice :: ‹('a ⇒ 'a) ⇒ 'a ⇒ 'a› where
9
9
‹twice f x = f (f x)›}
10
-
\shiki{lemma ‹rpt (twice f) n (f (x::two)) = f x›}
10
+
\shiki{lemma ‹rpt (twice f) n (f (x::oot)) = f x›}
11
11
\solnblock{
12
12
\shiki{apply (unfold twice_def)
13
13
apply (induct n)