# HG changeset patch
# User blanchet
# Date 1366729994 -7200
# Node ID 0468af6546ff2e81fdb02b13dfc1ca0507c7bf1c
# Parent  51f1f4ba18f36bb9d1681fec2b0c4fd99dd0cec4
more examples

diff -r 51f1f4ba18f3 -r 0468af6546ff src/HOL/BNF/Examples/Misc_Data.thy
--- a/src/HOL/BNF/Examples/Misc_Data.thy	Tue Apr 23 16:49:14 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Tue Apr 23 17:13:14 2013 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOL/BNF/Examples/Misc_Data.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
 
 Miscellaneous datatype declarations.
 *)
@@ -153,4 +154,25 @@
 data 'a dead_foo = A
 data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
 
+data d1 = D
+data d1' = is_D: D
+
+data d2 = D nat
+data d2' = is_D: D nat
+
+data d3 = D | E
+data d3' = D | is_E: E
+data d3'' = is_D: D | E
+data d3''' = is_D: D | is_E: E
+
+data d4 = D nat | E
+data d4' = D nat | is_E: E
+data d4'' = is_D: D nat | E
+data d4''' = is_D: D nat | is_E: E
+
+data d5 = D nat | E int
+data d5' = D nat | is_E: E int
+data d5'' = is_D: D nat | E int
+data d5''' = is_D: D nat | is_E: E int
+
 end