# HG changeset patch
# User bulwahn
# Date 1284109150 -7200
# Node ID dd84daec5d3c6cd8d6307443a0b3a3b0b5acf1d7
# Parent  b17ffa9652234bee2c3a89e2c739cc702d496ec0
adding another String.literal example

diff -r b17ffa965223 -r dd84daec5d3c src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 10 10:59:09 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 10 10:59:10 2010 +0200
@@ -1501,6 +1501,27 @@
 
 thm is_error.equation
 
+inductive is_error' :: "String.literal \<Rightarrow> bool"
+where
+  "is_error' (STR ''Error1'')"
+| "is_error' (STR ''Error2'')"
+
+code_pred is_error' .
+
+thm is_error'.equation
+
+datatype ErrorObject = Error String.literal int
+
+inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
+where
+  "is_error'' (Error Error_1 3)"
+| "is_error'' (Error Error_2 4)"
+
+code_pred is_error'' .
+
+thm is_error''.equation
+
+
 section {* Examples for detecting switches *}
 
 inductive detect_switches1 where