src/HOL/Record.thy
changeset 22759 e4a3f49eb924
parent 22744 5cbe966d67a2
child 22817 9dfadec17cc4
     1.1 --- a/src/HOL/Record.thy	Fri Apr 20 17:58:24 2007 +0200
     1.2 +++ b/src/HOL/Record.thy	Fri Apr 20 17:58:25 2007 +0200
     1.3 @@ -17,10 +17,9 @@
     1.4  lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
     1.5    by simp
     1.6  
     1.7 -definition
     1.8 +constdefs
     1.9    K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    1.10 -where
    1.11 -  K_record_apply [simp]: "K_record c x = c"
    1.12 +  K_record_apply [simp, code func]: "K_record c x \<equiv> c"
    1.13  
    1.14  lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
    1.15    by (rule ext) (simp add: K_record_apply comp_def)