--- a/src/HOL/HOL.thy Mon Feb 21 10:42:29 2011 +0100
+++ b/src/HOL/HOL.thy Mon Feb 21 10:44:19 2011 +0100
@@ -1111,7 +1111,8 @@
lemma if_eq_cancel: "(if x = y then y else x) = x"
by (simplesubst split_if, blast)
-lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
+lemma if_bool_eq_conj:
+"(if P then Q else R) = ((P-->Q) & (~P-->R))"
-- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
by (rule split_if)
@@ -1990,9 +1991,9 @@
subsubsection {* Nitpick setup *}
ML {*
-structure Nitpick_Defs = Named_Thms
+structure Nitpick_Unfolds = Named_Thms
(
- val name = "nitpick_def"
+ val name = "nitpick_unfold"
val description = "alternative definitions of constants as needed by Nitpick"
)
structure Nitpick_Simps = Named_Thms
@@ -2013,12 +2014,15 @@
*}
setup {*
- Nitpick_Defs.setup
+ Nitpick_Unfolds.setup
#> Nitpick_Simps.setup
#> Nitpick_Psimps.setup
#> Nitpick_Choice_Specs.setup
*}
+declare if_bool_eq_conj [nitpick_unfold, no_atp]
+ if_bool_eq_disj [no_atp]
+
subsection {* Preprocessing for the predicate compiler *}