1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
     1.3 @@ -789,7 +789,6 @@
     1.4  
     1.5  code_pred [inductify, skip_proof] case_f .
     1.6  thm case_fP.equation
     1.7 -thm case_fP.intros
     1.8  
     1.9  fun fold_map_idx where
    1.10    "fold_map_idx f i y [] = (y, [])"
    1.11 @@ -935,10 +934,10 @@
    1.12  code_pred [inductify] avl .
    1.13  thm avl.equation*)
    1.14  
    1.15 -code_pred [random_dseq inductify] avl .
    1.16 -thm avl.random_dseq_equation
    1.17 +code_pred [new_random_dseq inductify] avl .
    1.18 +thm avl.new_random_dseq_equation
    1.19  
    1.20 -values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
    1.21 +values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
    1.22  
    1.23  fun set_of
    1.24  where

     2.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  definition
     2.5    "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
     2.6  
     2.7 -code_pred (expected_modes: i => bool) [inductify] greater_than_index .
     2.8 +code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
     2.9  ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
    2.10  
    2.11  thm greater_than_index.equation
    2.12 @@ -38,7 +38,7 @@
    2.13  
    2.14  text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
    2.15  
    2.16 -code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
    2.17 +code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
    2.18  
    2.19  thm max_of_my_SucP.equation
    2.20  
    2.21 @@ -218,7 +218,7 @@
    2.22      \<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>"
    2.23  | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
    2.24  
    2.25 -code_pred [inductify, skip_proof] typing .
    2.26 +code_pred [inductify, skip_proof, specialise] typing .
    2.27  
    2.28  thm typing.equation
    2.29