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.
mutabelle ignores theorems with internal constants
authorbulwahn
Sun, 05 Feb 2012 17:43:14 +0100
changeset 46433 b67bb064de1e
parent 46432 ce8f7944fd6b
child 46434 6d2af424d0f8
mutabelle ignores theorems with internal constants
src/HOL/Mutabelle/mutabelle_extra.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:09:21 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:43:14 2012 +0100
@@ -241,7 +241,8 @@
   "nibble"]
 
 val forbidden_consts =
- [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
+ [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
+  @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in
isabelle