# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID cc0bae788b7eb70f0f7ad9440117d01a441f7196
# Parent  462b1dd67a58ece27415bec063dc6deddca81842
added a new example for the predicate compiler

diff -r 462b1dd67a58 -r cc0bae788b7e src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -181,17 +181,22 @@
 
 value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
 
-subsection {* Executing definitions *}
+section {* Executing definitions *}
 
 definition Min
 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
 
 code_pred (inductify_all) Min .
 
+subsection {* Examples with lists *}
+
 code_pred (inductify_all) lexord .
 
 thm lexord.equation
-
+(*
+lemma "(u, v) : lexord r ==> (x @ u, x @ v) : lexord r"
+quickcheck
+*)
 
 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
 
@@ -204,6 +209,10 @@
 code_pred (inductify_all) (rpred) lenlex .
 thm lenlex.rpred_equation
 *)
+thm lists.intros
+code_pred (inductify_all) lists .
+
+thm lists.equation
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
 fun height :: "'a tree => nat" where