adding some forbidden constant names for mutabelle
authorbulwahn
Sun, 05 Feb 2012 17:43:15 +0100
changeset 46434 6d2af424d0f8
parent 46433 b67bb064de1e
child 46435 e9c90516bc0d
adding some forbidden constant names for mutabelle
src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:43:14 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:43:15 2012 +0100
@@ -281,7 +281,8 @@
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
  @{const_name Quickcheck.catch_match},
- @{const_name Quickcheck_Exhaustive.unknown}
+ @{const_name Quickcheck_Exhaustive.unknown},
+ @{const_name Int.Bit0}, @{const_name Int.Bit1}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =