tuned;
authorwenzelm
Thu Jul 05 20:01:35 2007 +0200 (2007-07-05)
changeset 23598e03a43b8178c
parent 23597 ab67175ca8a5
child 23599 d889725b0d8a
tuned;
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
     1.3 @@ -107,8 +107,7 @@
     1.4    val debug_bounds: bool ref
     1.5    val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
     1.6    val set_solvers: solver list -> simpset -> simpset
     1.7 -  val rewrite_cterm: bool * bool * bool ->
     1.8 -    (simpset -> thm -> thm option) -> simpset -> cterm -> thm
     1.9 +  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
    1.10    val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
    1.11    val rewrite_thm: bool * bool * bool ->
    1.12      (simpset -> thm -> thm option) -> simpset -> thm -> thm
    1.13 @@ -118,7 +117,7 @@
    1.14      (simpset -> tactic) -> simpset -> int -> tactic
    1.15    val norm_hhf: thm -> thm
    1.16    val norm_hhf_protect: thm -> thm
    1.17 -  val rewrite: bool -> thm list -> cterm -> thm
    1.18 +  val rewrite: bool -> thm list -> conv
    1.19    val simplify: bool -> thm list -> thm -> thm
    1.20  end;
    1.21  
    1.22 @@ -1256,11 +1255,7 @@
    1.23          (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
    1.24  
    1.25  (*Rewrite a theorem*)
    1.26 -fun simplify _ [] th = th
    1.27 -  | simplify full thms th =
    1.28 -      Conv.fconv_rule (rewrite_cterm (full, false, false) simple_prover
    1.29 -        (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
    1.30 -
    1.31 +fun simplify full thms = Conv.fconv_rule (rewrite full thms);
    1.32  val rewrite_rule = simplify true;
    1.33  
    1.34  (*simple term rewriting -- no proof*)
     2.1 --- a/src/Pure/simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
     2.2 +++ b/src/Pure/simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
     2.3 @@ -55,11 +55,11 @@
     2.4      -> (theory -> simpset -> term -> thm option) -> simproc
     2.5    val simproc: theory -> string -> string list
     2.6      -> (theory -> simpset -> term -> thm option) -> simproc
     2.7 -  val          rewrite: simpset -> cterm -> thm
     2.8 -  val      asm_rewrite: simpset -> cterm -> thm
     2.9 -  val     full_rewrite: simpset -> cterm -> thm
    2.10 -  val   asm_lr_rewrite: simpset -> cterm -> thm
    2.11 -  val asm_full_rewrite: simpset -> cterm -> thm
    2.12 +  val          rewrite: simpset -> conv
    2.13 +  val      asm_rewrite: simpset -> conv
    2.14 +  val     full_rewrite: simpset -> conv
    2.15 +  val   asm_lr_rewrite: simpset -> conv
    2.16 +  val asm_full_rewrite: simpset -> conv
    2.17    val get_simpset: theory -> simpset
    2.18    val print_local_simpset: Proof.context -> unit
    2.19    val get_local_simpset: Proof.context -> simpset