merged
authorboehmes
Mon, 21 Sep 2009 11:15:55 +0200
changeset 32623 d84b1b0077ae
parent 32622 8ed38c7bd21a (diff)
parent 32621 a073cb249a06 (current diff)
child 32625 f270520df7de
merged
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/HoareParallel/OG_Com.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/OG_Hoare.thy
src/HOL/HoareParallel/OG_Syntax.thy
src/HOL/HoareParallel/OG_Tactics.thy
src/HOL/HoareParallel/OG_Tran.thy
src/HOL/HoareParallel/Quote_Antiquote.thy
src/HOL/HoareParallel/RG_Com.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/HoareParallel/RG_Syntax.thy
src/HOL/HoareParallel/RG_Tran.thy
src/HOL/HoareParallel/ROOT.ML
src/HOL/HoareParallel/document/root.bib
src/HOL/HoareParallel/document/root.tex
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Sep 21 11:15:55 2009 +0200
@@ -9,7 +9,7 @@
 begin
 
 declare [[smt_solver=z3, z3_proofs=false]]
-declare [[smt_trace=true]] (*FIXME*)
+declare [[smt_trace=false]]
 
 
 section {* Propositional and first-order logic *}
@@ -163,6 +163,7 @@
    (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
+  using [[smt_solver=z3]]
   by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
 
 
--- a/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 11:15:55 2009 +0200
@@ -121,7 +121,7 @@
     fun cmd f1 f2 =
       if path <> ""
       then map qq (path :: args) @ [qf f1, ">", qf f2]
-      else map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
+      else "perl -w" :: map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
   in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
 
 end
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl	Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Mon Sep 21 11:15:55 2009 +0200
@@ -1,4 +1,3 @@
-#!/usr/bin/env perl -w
 #
 # Script to invoke remote SMT solvers.
 # Author: Sascha Boehme, TU Muenchen