# HG changeset patch
# User bulwahn
# Date 1271844652 -7200
# Node ID 3f3e9f18f30211834377e1f542984df4459021c6
# Parent  d1d9dee7a4bf20a0152bb43c933ceaa78731d8c2
adopting examples to changes in the predicate compiler

diff -r d1d9dee7a4bf -r 3f3e9f18f302 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
@@ -789,7 +789,6 @@
 
 code_pred [inductify, skip_proof] case_f .
 thm case_fP.equation
-thm case_fP.intros
 
 fun fold_map_idx where
   "fold_map_idx f i y [] = (y, [])"
@@ -935,10 +934,10 @@
 code_pred [inductify] avl .
 thm avl.equation*)
 
-code_pred [random_dseq inductify] avl .
-thm avl.random_dseq_equation
+code_pred [new_random_dseq inductify] avl .
+thm avl.new_random_dseq_equation
 
-values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
+values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
 
 fun set_of
 where
diff -r d1d9dee7a4bf -r 3f3e9f18f302 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
@@ -12,7 +12,7 @@
 definition
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
-code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
 ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
@@ -38,7 +38,7 @@
 
 text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
 
-code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
 
 thm max_of_my_SucP.equation
 
@@ -218,7 +218,7 @@
     \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
 | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 
-code_pred [inductify, skip_proof] typing .
+code_pred [inductify, skip_proof, specialise] typing .
 
 thm typing.equation