# HG changeset patch
# User traytel
# Date 1364123251 -3600
# Node ID fce7243c5e773f7a3179b6163590554a7094e7d8
# Parent  01fe31f05aa8d6cd17d7bc110b95a95da40ffa8e
simple case syntax for stream (stolen from AFP/Coinductive)

diff -r 01fe31f05aa8 -r fce7243c5e77 src/HOL/BNF/Examples/Stream.thy
--- 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