predicate compiler: ignore Abs_filter and Rep_filter
authorhoelzl
Mon, 13 Apr 2015 12:15:29 +0200
changeset 60045 cd2b6debac18
parent 60044 7c4a2e87e4d0
child 60046 894d6d863823
predicate compiler: ignore Abs_filter and Rep_filter
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 13 12:13:52 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 13 12:15:29 2015 +0200
@@ -24,6 +24,11 @@
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *}
 
+section {* Filters *}
+
+(*TODO: shouldn't this be done by typedef? *)
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}] *}
+
 section {* Bounded quantifiers *}
 
 declare Ball_def[code_pred_inline]