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.
ignoring the constant STR in the predicate compiler
authorbulwahn
Mon, 15 Nov 2010 13:40:12 +0100
changeset 40548 54eb5fd36e5e
parent 40540 293f9f211be0
child 40549 63a3c8539d41
ignoring the constant STR in the predicate compiler
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 00:20:36 2010 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 13:40:12 2010 +0100
@@ -244,6 +244,10 @@
     done
 qed
 
+section {* Setup for String.literal *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
+
 section {* Simplification rules for optimisation *}
 
 lemma [code_pred_simp]: "\<not> False == True"
isabelle