src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 40548 54eb5fd36e5e
parent 40054 cd7b1fa20bce
child 41075 4bed56dc95fb
     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"