removed unused Predicate_Compile_Set
authorbulwahn
Mon Mar 22 08:30:13 2010 +0100 (2010-03-22)
changeset 3589014a0993fe64b
parent 35889 c1f86c5d3827
child 35891 3122bdd95275
removed unused Predicate_Compile_Set
src/HOL/IsaMakefile
src/HOL/Predicate_Compile.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -301,7 +301,6 @@
     1.4    Tools/Predicate_Compile/predicate_compile_fun.ML \
     1.5    Tools/Predicate_Compile/predicate_compile.ML \
     1.6    Tools/Predicate_Compile/predicate_compile_pred.ML \
     1.7 -  Tools/Predicate_Compile/predicate_compile_set.ML \
     1.8    Tools/quickcheck_generators.ML \
     1.9    Tools/Qelim/cooper_data.ML \
    1.10    Tools/Qelim/cooper.ML \
     2.1 --- a/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
     2.3 @@ -10,7 +10,6 @@
     2.4  uses
     2.5    "Tools/Predicate_Compile/predicate_compile_aux.ML"
     2.6    "Tools/Predicate_Compile/predicate_compile_core.ML"
     2.7 -  "Tools/Predicate_Compile/predicate_compile_set.ML"
     2.8    "Tools/Predicate_Compile/predicate_compile_data.ML"
     2.9    "Tools/Predicate_Compile/predicate_compile_fun.ML"
    2.10    "Tools/Predicate_Compile/predicate_compile_pred.ML"
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML	Mon Mar 22 08:30:13 2010 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,53 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_set.ML
     3.5 -    Author:     Lukas Bulwahn, TU Muenchen
     3.6 -
     3.7 -Preprocessing sets to predicates.
     3.8 -*)
     3.9 -
    3.10 -signature PREDICATE_COMPILE_SET =
    3.11 -sig
    3.12 -(*
    3.13 -  val preprocess_intro : thm -> theory -> thm * theory
    3.14 -  val preprocess_clause : term -> theory -> term * theory
    3.15 -*)
    3.16 -  val unfold_set_notation : thm -> thm;
    3.17 -end;
    3.18 -
    3.19 -structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
    3.20 -struct
    3.21 -(*FIXME: unfolding Ball in pretty adhoc here *)
    3.22 -val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
    3.23 -@{thm Ball_def}, @{thm Bex_def}]
    3.24 -
    3.25 -val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
    3.26 -
    3.27 -(*
    3.28 -fun find_set_theorems ctxt cname =
    3.29 -  let
    3.30 -    val _ = cname 
    3.31 -*)
    3.32 -
    3.33 -(*
    3.34 -fun preprocess_term t ctxt =
    3.35 -  case t of
    3.36 -    Const ("op :", _) $ x $ A => 
    3.37 -      case strip_comb A of
    3.38 -        (Const (cname, T), params) =>
    3.39 -          let 
    3.40 -            val _ = find_set_theorems
    3.41 -          in
    3.42 -            (t, ctxt)
    3.43 -          end
    3.44 -      | _ => (t, ctxt)  
    3.45 -  | _ => (t, ctxt)
    3.46 -*) 
    3.47 -(*
    3.48 -fun preprocess_intro th thy =
    3.49 -  let
    3.50 -    val cnames = find_heads_of_prems
    3.51 -    val set_cname = filter (has_set_definition
    3.52 -    val _ = define_preds
    3.53 -    val _ = prep_pred_def
    3.54 -  in
    3.55 -*)
    3.56 -end;