tuned code annotations
authorhaftmann
Tue Jul 14 16:27:31 2009 +0200 (2009-07-14)
changeset 3206898acc234d683
parent 32067 e425fe0ff24a
child 32069 6d28bbd33e2c
tuned code annotations
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Jul 14 16:27:30 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jul 14 16:27:31 2009 +0200
     1.3 @@ -187,8 +187,8 @@
     1.4    True_or_False:  "(P=True) | (P=False)"
     1.5  
     1.6  defs
     1.7 -  Let_def:      "Let s f == f(s)"
     1.8 -  if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.9 +  Let_def [code]: "Let s f == f(s)"
    1.10 +  if_def:         "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
    1.11  
    1.12  finalconsts
    1.13    "op ="
    1.14 @@ -1029,8 +1029,8 @@
    1.15      "(P ~= Q) = (P = (~Q))"
    1.16      "(P | ~P) = True"    "(~P | P) = True"
    1.17      "(x = x) = True"
    1.18 -  and not_True_eq_False: "(\<not> True) = False"
    1.19 -  and not_False_eq_True: "(\<not> False) = True"
    1.20 +  and not_True_eq_False [code]: "(\<not> True) = False"
    1.21 +  and not_False_eq_True [code]: "(\<not> False) = True"
    1.22    and
    1.23      "(~P) ~= P"  "P ~= (~P)"
    1.24      "(True=P) = P"
    1.25 @@ -1157,10 +1157,10 @@
    1.26  
    1.27  text {* \medskip if-then-else rules *}
    1.28  
    1.29 -lemma if_True: "(if True then x else y) = x"
    1.30 +lemma if_True [code]: "(if True then x else y) = x"
    1.31    by (unfold if_def) blast
    1.32  
    1.33 -lemma if_False: "(if False then x else y) = y"
    1.34 +lemma if_False [code]: "(if False then x else y) = y"
    1.35    by (unfold if_def) blast
    1.36  
    1.37  lemma if_P: "P ==> (if P then x else y) = x"
    1.38 @@ -1722,6 +1722,7 @@
    1.39  setup {*
    1.40    Codegen.setup
    1.41    #> RecfunCodegen.setup
    1.42 +  #> Codegen.map_unfold (K HOL_basic_ss)
    1.43  *}
    1.44  
    1.45  types_code
    1.46 @@ -1841,13 +1842,7 @@
    1.47      and "x \<or> False \<longleftrightarrow> x"
    1.48      and "x \<or> True \<longleftrightarrow> True" by simp_all
    1.49  
    1.50 -lemma [code]:
    1.51 -  shows "\<not> True \<longleftrightarrow> False"
    1.52 -    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    1.53 -
    1.54 -lemmas [code] = Let_def if_True if_False
    1.55 -
    1.56 -lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
    1.57 +declare imp_conv_disj [code, code_unfold_post]
    1.58  
    1.59  instantiation itself :: (type) eq
    1.60  begin