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.
added rewrite_cterm;
authorwenzelm
Thu, 25 Jun 1998 15:20:59 +0200
changeset 5079 2a8ed71f791f
parent 5078 7b5ea59c0275
child 5080 ce093ff0880e
added rewrite_cterm;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Thu Jun 25 13:57:34 1998 +0200
+++ b/src/Pure/drule.ML	Thu Jun 25 15:20:59 1998 +0200
@@ -56,6 +56,9 @@
   val rewrite_thm	: bool * bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> thm -> thm
+  val rewrite_cterm	: bool * bool * bool
+                          -> (meta_simpset -> thm -> thm option)
+                          -> meta_simpset -> cterm -> thm
   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_goal_rule	: bool* bool * bool
                           -> (meta_simpset -> thm -> thm option)
@@ -452,6 +455,7 @@
       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
 
 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
+fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
 fun rewrite_goals_rule_aux _ []   th = th
isabelle