Thu, 03 Apr 2014 19:49:53 +0200 wenzelm slightly more readable protocol trace (NB1: prover input is always marked as <prover_command/>; NB2: adding indentation would invalidate the XML);
Thu, 03 Apr 2014 19:26:39 +0200 wenzelm recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
Thu, 03 Apr 2014 18:39:42 +0200 wenzelm tuned rendering for 5 different look-and-feels;
Thu, 03 Apr 2014 15:40:31 +0200 wenzelm more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy or HOL/Library/Monad_Syntax.thy;
Thu, 03 Apr 2014 14:54:17 +0200 wenzelm more general prover operations;
Thu, 03 Apr 2014 13:49:37 +0200 wenzelm tuned signature -- pro forma;
Thu, 03 Apr 2014 13:46:18 +0200 wenzelm more general prover operations;
Thu, 03 Apr 2014 17:26:45 +0100 paulson Merge
Thu, 03 Apr 2014 17:26:04 +0100 paulson Cleaned up some messy proofs
Thu, 03 Apr 2014 18:24:08 +0200 hoelzl fix #0556204bc230
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Thu, 03 Apr 2014 17:16:02 +0200 blanchet don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
Thu, 03 Apr 2014 17:00:14 +0200 blanchet use Alt-Ergo 0.95.2, the latest and greatest version
Thu, 03 Apr 2014 16:57:19 +0200 blanchet updated Z3 TPTP to 4.3.1+
Thu, 03 Apr 2014 13:29:58 +0200 blanchet updated Why3 version in docs
Thu, 03 Apr 2014 10:51:24 +0200 blanchet added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
(0) -30000 -10000 -3000 -1000 -300 -100 -16 +16 +100 +300 +1000 +3000 +10000 tip