src/HOL/HOL.thy
changeset 41792 ff3cb0c418b7
parent 41636 934b4ad9b611
child 41827 98eda7ffde79
     1.1 --- a/src/HOL/HOL.thy	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -1111,7 +1111,8 @@
     1.4  lemma if_eq_cancel: "(if x = y then y else x) = x"
     1.5  by (simplesubst split_if, blast)
     1.6  
     1.7 -lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
     1.8 +lemma if_bool_eq_conj:
     1.9 +"(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.10    -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
    1.11    by (rule split_if)
    1.12  
    1.13 @@ -1990,9 +1991,9 @@
    1.14  subsubsection {* Nitpick setup *}
    1.15  
    1.16  ML {*
    1.17 -structure Nitpick_Defs = Named_Thms
    1.18 +structure Nitpick_Unfolds = Named_Thms
    1.19  (
    1.20 -  val name = "nitpick_def"
    1.21 +  val name = "nitpick_unfold"
    1.22    val description = "alternative definitions of constants as needed by Nitpick"
    1.23  )
    1.24  structure Nitpick_Simps = Named_Thms
    1.25 @@ -2013,12 +2014,15 @@
    1.26  *}
    1.27  
    1.28  setup {*
    1.29 -  Nitpick_Defs.setup
    1.30 +  Nitpick_Unfolds.setup
    1.31    #> Nitpick_Simps.setup
    1.32    #> Nitpick_Psimps.setup
    1.33    #> Nitpick_Choice_Specs.setup
    1.34  *}
    1.35  
    1.36 +declare if_bool_eq_conj [nitpick_unfold, no_atp]
    1.37 +        if_bool_eq_disj [no_atp]
    1.38 +
    1.39  
    1.40  subsection {* Preprocessing for the predicate compiler *}
    1.41