Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/tactic.ML
changeset 7596 c97c3ad15d2e
parent 7491 95a4af0e10a7
child 8129 29e239c7b8c2 
--- a/src/Pure/tactic.ML	Fri Sep 24 17:18:51 1999 +0200
+++ b/src/Pure/tactic.ML	Sat Sep 25 13:05:38 1999 +0200
@@ -49,6 +49,7 @@
   val filt_resolve_tac	: thm list -> int -> int -> tactic
   val flexflex_tac	: tactic
   val fold_goals_tac	: thm list -> tactic
+  val fold_rule		: thm list -> thm -> thm
   val fold_tac		: thm list -> tactic
   val forward_tac	: thm list -> int -> tactic   
   val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
@@ -509,11 +510,11 @@
       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   in  map (keyfilter keylist) keys  end;
 
-fun fold_tac defs = EVERY 
-    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
+val rev_defs = sort_lhs_depths o map symmetric;
 
-fun fold_goals_tac defs = EVERY 
-    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
+fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
+fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
+fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 
 
 (*** Renaming of parameters in a subgoal
isabelle