# HG changeset patch
# User blanchet
# Date 1348758054 -7200
# Node ID 7ec6471f8388942b0bb8daa11a18575417c26b4e
# Parent  788a32befa2ea54bb5a250d72f0ce1bd05eedd81
modernized examples

diff -r 788a32befa2e -r 7ec6471f8388 src/HOL/BNF/Examples/Misc_Codata.thy
--- a/src/HOL/BNF/Examples/Misc_Codata.thy	Thu Sep 27 12:08:38 2012 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy	Thu Sep 27 17:00:54 2012 +0200
@@ -58,11 +58,15 @@
    and ('a, 'b, 'c) in_here =
   IH1 'b 'a | IH2 'c
 
-codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
-and in_here': 'c = "'d + 'e"
+codata ('a, 'b, 'c) some_killing' =
+  SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'"
+   and ('a, 'b, 'c) in_here' =
+  IH1' 'b | IH2' 'c
 
-codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
-and in_here'': 'c = "'d \<times> 'b + 'e"
+codata ('a, 'b, 'c) some_killing'' =
+  SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''"
+   and ('a, 'b, 'c) in_here'' =
+  IH1'' 'b 'a | IH2'' 'c
 
 codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"