--- a/src/HOL/IsaMakefile Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 22 08:30:13 2010 +0100
@@ -301,7 +301,6 @@
Tools/Predicate_Compile/predicate_compile_fun.ML \
Tools/Predicate_Compile/predicate_compile.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
- Tools/Predicate_Compile/predicate_compile_set.ML \
Tools/quickcheck_generators.ML \
Tools/Qelim/cooper_data.ML \
Tools/Qelim/cooper.ML \
--- a/src/HOL/Predicate_Compile.thy Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Predicate_Compile.thy Mon Mar 22 08:30:13 2010 +0100
@@ -10,7 +10,6 @@
uses
"Tools/Predicate_Compile/predicate_compile_aux.ML"
"Tools/Predicate_Compile/predicate_compile_core.ML"
- "Tools/Predicate_Compile/predicate_compile_set.ML"
"Tools/Predicate_Compile/predicate_compile_data.ML"
"Tools/Predicate_Compile/predicate_compile_fun.ML"
"Tools/Predicate_Compile/predicate_compile_pred.ML"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML Mon Mar 22 08:30:13 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: HOL/Tools/Predicate_Compile/predicate_compile_set.ML
- Author: Lukas Bulwahn, TU Muenchen
-
-Preprocessing sets to predicates.
-*)
-
-signature PREDICATE_COMPILE_SET =
-sig
-(*
- val preprocess_intro : thm -> theory -> thm * theory
- val preprocess_clause : term -> theory -> term * theory
-*)
- val unfold_set_notation : thm -> thm;
-end;
-
-structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
-struct
-(*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
-@{thm Ball_def}, @{thm Bex_def}]
-
-val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
-
-(*
-fun find_set_theorems ctxt cname =
- let
- val _ = cname
-*)
-
-(*
-fun preprocess_term t ctxt =
- case t of
- Const ("op :", _) $ x $ A =>
- case strip_comb A of
- (Const (cname, T), params) =>
- let
- val _ = find_set_theorems
- in
- (t, ctxt)
- end
- | _ => (t, ctxt)
- | _ => (t, ctxt)
-*)
-(*
-fun preprocess_intro th thy =
- let
- val cnames = find_heads_of_prems
- val set_cname = filter (has_set_definition
- val _ = define_preds
- val _ = prep_pred_def
- in
-*)
-end;