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.
Fix: Auto term must apply wf-intro rules repeatedly.
authorkrauss
Thu, 11 May 2006 11:11:05 +0200
changeset 19610 93dc5e63d05e
parent 19609 a677ac8c9b10
child 19611 da2a0014c461
Fix: Auto term must apply wf-intro rules repeatedly.
src/HOL/Tools/function_package/auto_term.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/auto_term.ML	Thu May 11 10:25:55 2006 +0200
+++ b/src/HOL/Tools/function_package/auto_term.ML	Thu May 11 11:11:05 2006 +0200
@@ -24,7 +24,7 @@
     (resolve_tac [tc_intro_rule] 1)                    (* produce the usual goals *)
         THEN (instantiate_tac [("R", relstr)])    (* instantiate with the given relation *)
 	THEN (ALLGOALS 
-		  (fn 1 => ares_tac wf_rules 1    (* Solve wellfoundedness *)
+		  (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
 		    | i => asm_simp_tac ss i))    (* Simplify termination conditions *)
 
 fun mk_termination_meth relstr ctxt =
isabelle