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.
don't relearn old facts in Isar mode
authorblanchet
Mon, 23 Jul 2012 15:32:30 +0200
changeset 48433 9e9b6e363859
parent 48432 60759d07df24
child 48434 aaaec69db3db
don't relearn old facts in Isar mode
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -29,7 +29,7 @@
 open Sledgehammer_MaSh
 open Sledgehammer_Run
 
-val cvc3N = "cvc3"
+(* val cvc3N = "cvc3" *)
 val yicesN = "yices"
 val z3N = "z3"
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -774,7 +774,7 @@
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
             in (reps, (n, next_commit, timed_out)) end
         val n =
-          if null old_facts then
+          if not atp orelse null old_facts then
             n
           else
             let
isabelle