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