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.
lexicographic order: run local descent proofs in parallel
authorkrauss
Mon, 02 Nov 2009 23:06:06 +0100
changeset 33398 daa526c9e5d2
parent 33397 609389f3ea1e
child 33402 d9a25a87da4a
lexicographic order: run local descent proofs in parallel
src/HOL/Tools/Function/lexicographic_order.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 13:43:50 2009 -0800
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 23:06:06 2009 +0100
@@ -197,7 +197,7 @@
       val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
 
       (* 2: create table *)
-      val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+      val table = Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
     in
       case search_table table of
         NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
isabelle