--- a/src/HOL/BNF/Examples/Stream.thy Sat Mar 23 21:48:03 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy Sun Mar 24 12:07:31 2013 +0100
@@ -30,6 +30,9 @@
end
*)
*}
+translations -- "poor man's case syntax"
+ "case p of XCONST Stream x s \<Rightarrow> b" \<rightleftharpoons> "CONST stream_case (\<lambda>x s. b) p"
+ "case p of (XCONST Stream :: 'b) x s \<Rightarrow> b" \<rightharpoonup>" CONST stream_case (\<lambda>x s. b) p"
code_datatype Stream
lemmas [code] = stream.sels stream.sets stream.case