Thu, 06 Jan 2011 17:51:56 +0100 | boehmes | differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); | file | diff | annotate |
Wed, 24 Nov 2010 16:15:15 +0100 | blanchet | more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers | file | diff | annotate |
Wed, 12 May 2010 23:54:02 +0200 | boehmes | integrated SMT into the HOL image | file | diff | annotate |