Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mutabelle/mutabelle_extra.ML
changeset 42435 c3d880b13aa9
parent 42361 23f352990944
child 42438 cf963c834435 
--- 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