src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 36040 fcd7bea01a93
parent 36033 7106f079bd05
child 36054 93d62439506c
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Mar 29 17:30:55 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Mar 29 17:30:56 2010 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4      \<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.5  | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
     1.6  
     1.7 -code_pred [inductify] typing .
     1.8 +code_pred [inductify, skip_proof] typing .
     1.9  
    1.10  thm typing.equation
    1.11