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 two further code-generator internal constants to the blacklist of Mutabelle
authorbulwahn
Wed, 20 Apr 2011 16:00:46 +0200
changeset 42435 c3d880b13aa9
parent 42434 1914fd5d7c0e
child 42437 4344b3654961
adding two further code-generator internal constants to the blacklist of Mutabelle
src/HOL/Mutabelle/mutabelle_extra.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:00:45 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:00:46 2011 +0200
@@ -273,7 +273,9 @@
  @{const_name "ord_fun_inst.less_fun"},
  @{const_name Metis.fequal},
  @{const_name Meson.skolem},
- @{const_name transfer_morphism}
+ @{const_name transfer_morphism},
+ @{const_name enum_prod_inst.enum_all_prod},
+ @{const_name enum_prod_inst.enum_ex_prod}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
isabelle