--- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(* 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;