src/HOL/ex/ExecutableContent.thy
changeset 30332 0d07f4823d3a
parent 30328 ab47f43f7581
child 30428 14f469e70eab
equal deleted inserted replaced
30331:32ccef17d408 30332:0d07f4823d3a
    22   Word
    22   Word
    23   "~~/src/HOL/ex/Commutative_Ring_Complete"
    23   "~~/src/HOL/ex/Commutative_Ring_Complete"
    24   "~~/src/HOL/ex/Records"
    24   "~~/src/HOL/ex/Records"
    25 begin
    25 begin
    26 
    26 
    27 lemma [code, code del]: "(term_of \<Colon> 'a Predicate.pred \<Rightarrow> term) = term_of" ..
    27 lemma [code, code del]:
       
    28   "(size :: 'a::size Predicate.pred => nat) = size" ..
       
    29 lemma [code, code del]:
       
    30   "pred_size = pred_size" ..
       
    31 lemma [code, code del]:
       
    32   "pred_case = pred_case" ..
       
    33 lemma [code, code del]:
       
    34   "pred_rec = pred_rec" ..
       
    35 lemma [code, code del]:
       
    36   "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
       
    37 lemma [code, code del]:
       
    38   "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
    28 
    39 
    29 text {* However, some aren't executable *}
    40 text {* However, some aren't executable *}
    30 
    41 
    31 declare pair_leq_def[code del]
    42 declare pair_leq_def[code del]
    32 declare max_weak_def[code del]
    43 declare max_weak_def[code del]