src/HOL/Corec_Examples/Tests/Merge_Poly.thy
 changeset 62698 9d706e37ddab parent 62696 7325d8573fb8 child 62726 5b2a7caa855b
```     1.1 --- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Tue Mar 22 13:32:40 2016 +0100
1.2 +++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Tue Mar 22 13:44:50 2016 +0100
1.3 @@ -102,21 +102,21 @@
1.4  friend_of_corec h1 where
1.5    "h1 x = ACons undefined undefined" sorry
1.6
1.7 -friend_of_corec h2 where
1.8 -  "h2 x = (case x of
1.9 -    ACons a t \<Rightarrow> ACons a (h1 (h2 t))
1.10 +friend_of_corec h2 where
1.11 +  "h2 x = (case x of
1.12 +    ACons a t \<Rightarrow> ACons a (h1 (h2 t))
1.13    | BCons b t \<Rightarrow> BCons b (h1 (h2 t)))"
1.14    sorry
1.15
1.16  friend_of_corec h3 where
1.17 -  "h3 x = (case x of
1.18 -    ACons a t \<Rightarrow> ACons a (h1 (h3 t))
1.19 +  "h3 x = (case x of
1.20 +    ACons a t \<Rightarrow> ACons a (h1 (h3 t))
1.21    | BCons b t \<Rightarrow> BCons b (h1 (h3 t)))"
1.22    sorry
1.23
1.24  friend_of_corec h4 where
1.25 -  "h4 x = (case x of
1.26 -    ACons a t \<Rightarrow> ACons a (h1 (h4 t))
1.27 +  "h4 x = (case x of
1.28 +    ACons a t \<Rightarrow> ACons a (h1 (h4 t))
1.29    | BCons b t \<Rightarrow> BCons b (h1 (h4 t)))"
1.30    sorry
1.31
```