# HG changeset patch
# User haftmann
# Date 1253020935 -7200
# Node ID 73ad5dbf1034b1cc373ae430e784d8dce3ae3e7b
# Parent  22117a76f9435c3e1fa063f8511641c100e398cb
added singleton example

diff -r 22117a76f943 -r 73ad5dbf1034 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Sep 15 12:11:10 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Sep 15 15:22:15 2009 +0200
@@ -157,4 +157,13 @@
 values 3 "{(a,q). step (par nil nil) a q}"
 *)
 
+
+inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+    "k < l \<Longrightarrow> divmod_rel k l 0 k"
+  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
+
+code_pred divmod_rel ..
+
+value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+
 end
\ No newline at end of file