src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
 changeset 36257 3f3e9f18f302 parent 36054 93d62439506c child 37008 8da3b51726ac
```     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
1.3 @@ -12,7 +12,7 @@
1.4  definition
1.5    "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
1.6
1.7 -code_pred (expected_modes: i => bool) [inductify] greater_than_index .
1.8 +code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
1.9  ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
1.10
1.11  thm greater_than_index.equation
1.12 @@ -38,7 +38,7 @@
1.13
1.14  text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
1.15
1.16 -code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
1.17 +code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
1.18
1.19  thm max_of_my_SucP.equation
1.20
1.21 @@ -218,7 +218,7 @@
1.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>"
1.23  | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
1.24
1.25 -code_pred [inductify, skip_proof] typing .
1.26 +code_pred [inductify, skip_proof, specialise] typing .
1.27
1.28  thm typing.equation
1.29
```