src/HOL/Corec_Examples/Tests/Misc_Poly.thy
changeset 62698 9d706e37ddab
parent 62696 7325d8573fb8
child 62726 5b2a7caa855b
     1.1 --- a/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Tue Mar 22 13:32:40 2016 +0100
     1.2 +++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Tue Mar 22 13:44:50 2016 +0100
     1.3 @@ -260,7 +260,7 @@
     1.4    sorry
     1.5  
     1.6  corec f23 where
     1.7 -  "f23 xh = Node undefined 
     1.8 +  "f23 xh = Node undefined
     1.9      (if is_H1 xh then
    1.10        (f23 (h_tail xh)) # (branches (h_a xh))
    1.11      else if is_H1 xh then
    1.12 @@ -269,7 +269,7 @@
    1.13        [])"
    1.14  
    1.15  friend_of_corec f23 where
    1.16 -  "f23 xh = Node undefined 
    1.17 +  "f23 xh = Node undefined
    1.18      (if is_H1 xh then
    1.19        (f23 (h_tail xh)) # (branches (h_a xh))
    1.20      else if is_H1 xh then
    1.21 @@ -279,7 +279,7 @@
    1.22    sorry
    1.23  
    1.24  corec f24 where
    1.25 -  "f24 xh = 
    1.26 +  "f24 xh =
    1.27      (if is_H1 xh then
    1.28        Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
    1.29      else if is_H2 xh then
    1.30 @@ -288,7 +288,7 @@
    1.31        Node 0 [])"
    1.32  
    1.33  friend_of_corec f24 :: "(('b :: {zero}) \<Rightarrow> 'b tree list, 'b, 'b \<Rightarrow> 'b tree list) h \<Rightarrow> 'b tree" where
    1.34 -  "f24 xh = 
    1.35 +  "f24 xh =
    1.36      (if is_H1 xh then
    1.37        Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
    1.38      else if is_H2 xh then