Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 05 Jul 2007 20:01:35 +0200
changeset 23598 e03a43b8178c
parent 23597 ab67175ca8a5
child 23599 d889725b0d8a
tuned;
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions
src/Pure/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
@@ -107,8 +107,7 @@
   val debug_bounds: bool ref
   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   val set_solvers: solver list -> simpset -> simpset
-  val rewrite_cterm: bool * bool * bool ->
-    (simpset -> thm -> thm option) -> simpset -> cterm -> thm
+  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
   val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   val rewrite_thm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> thm -> thm
@@ -118,7 +117,7 @@
     (simpset -> tactic) -> simpset -> int -> tactic
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
-  val rewrite: bool -> thm list -> cterm -> thm
+  val rewrite: bool -> thm list -> conv
   val simplify: bool -> thm list -> thm -> thm
 end;
 
@@ -1256,11 +1255,7 @@
         (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 
 (*Rewrite a theorem*)
-fun simplify _ [] th = th
-  | simplify full thms th =
-      Conv.fconv_rule (rewrite_cterm (full, false, false) simple_prover
-        (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
-
+fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 val rewrite_rule = simplify true;
 
 (*simple term rewriting -- no proof*)
--- a/src/Pure/simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
+++ b/src/Pure/simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
@@ -55,11 +55,11 @@
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
-  val          rewrite: simpset -> cterm -> thm
-  val      asm_rewrite: simpset -> cterm -> thm
-  val     full_rewrite: simpset -> cterm -> thm
-  val   asm_lr_rewrite: simpset -> cterm -> thm
-  val asm_full_rewrite: simpset -> cterm -> thm
+  val          rewrite: simpset -> conv
+  val      asm_rewrite: simpset -> conv
+  val     full_rewrite: simpset -> conv
+  val   asm_lr_rewrite: simpset -> conv
+  val asm_full_rewrite: simpset -> conv
   val get_simpset: theory -> simpset
   val print_local_simpset: Proof.context -> unit
   val get_local_simpset: Proof.context -> simpset
isabelle