ignoring the constant STR in the predicate compiler
authorbulwahn
Mon Nov 15 13:40:12 2010 +0100 (2010-11-15)
changeset 4054854eb5fd36e5e
parent 40540 293f9f211be0
child 40549 63a3c8539d41
ignoring the constant STR in the predicate compiler
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 00:20:36 2010 +0100
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 13:40:12 2010 +0100
     1.3 @@ -244,6 +244,10 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 +section {* Setup for String.literal *}
     1.8 +
     1.9 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
    1.10 +
    1.11  section {* Simplification rules for optimisation *}
    1.12  
    1.13  lemma [code_pred_simp]: "\<not> False == True"