Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding another internal constant to mutabelle's blacklust
authorbulwahn
Mon, 23 Jan 2012 15:22:33 +0100
changeset 46315 40522961d4b1
parent 46314 f6532c597300
child 46316 1c9a548c0402
adding another internal constant to mutabelle's blacklust
src/HOL/Mutabelle/mutabelle_extra.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 23 14:08:55 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 23 15:22:33 2012 +0100
@@ -278,7 +278,8 @@
  @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
- @{const_name Quickcheck.catch_match}
+ @{const_name Quickcheck.catch_match},
+ @{const_name Quickcheck_Exhaustive.unknown}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
isabelle