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.
changed URL of SMT server,
authorboehmes
Wed, 11 Nov 2009 15:43:03 +0100
changeset 33610 43bf5773f92a
parent 33609 059cd49e4b1e
child 33614 ecc90891c474
changed URL of SMT server, added Z3 rewrite lemma
src/HOL/SMT/Z3.thy file | annotate | diff | comparison | revisions
src/HOL/SMT/etc/settings file | annotate | diff | comparison | revisions 
--- a/src/HOL/SMT/Z3.thy	Wed Nov 11 14:04:56 2009 +0000
+++ b/src/HOL/SMT/Z3.thy	Wed Nov 11 15:43:03 2009 +0100
@@ -21,6 +21,8 @@
   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   ring_distribs field_eq_simps if_True if_False
 
+lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast
+
 lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast
 lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast
 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast
--- a/src/HOL/SMT/etc/settings	Wed Nov 11 14:04:56 2009 +0000
+++ b/src/HOL/SMT/etc/settings	Wed Nov 11 15:43:03 2009 +0100
@@ -2,7 +2,7 @@
 
 REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"
 
-REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt"
+REMOTE_SMT_URL="http://smt.in.tum.de/smt"
 
 CERT_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/cert_smt.pl"
isabelle