src/HOL/HOL.thy
changeset 53146 3a93bc5d3370
parent 52654 06653152ea8b
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 22 17:19:51 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Aug 22 21:15:43 2013 +0200
     1.3 @@ -1695,12 +1695,22 @@
     1.4  
     1.5  subsubsection {* Generic code generator preprocessor setup *}
     1.6  
     1.7 +lemma conj_left_cong:
     1.8 +  "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
     1.9 +  by (fact arg_cong)
    1.10 +
    1.11 +lemma disj_left_cong:
    1.12 +  "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
    1.13 +  by (fact arg_cong)
    1.14 +
    1.15  setup {*
    1.16    Code_Preproc.map_pre (put_simpset HOL_basic_ss)
    1.17    #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
    1.18 -  #> Code_Simp.map_ss (put_simpset HOL_basic_ss)
    1.19 +  #> Code_Simp.map_ss (put_simpset HOL_basic_ss
    1.20 +    #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
    1.21  *}
    1.22  
    1.23 +
    1.24  subsubsection {* Equality *}
    1.25  
    1.26  class equal =