Tue, 17 Dec 2013 20:21:22 +0100 haftmann initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts
Tue, 17 Dec 2013 15:56:57 +0100 traytel reduced cardinals dependencies of (co)datatypes
Tue, 17 Dec 2013 15:44:10 +0100 traytel tighter bnf bounds for (co)datatypes
Tue, 17 Dec 2013 15:15:59 +0100 traytel tuned
Tue, 17 Dec 2013 14:22:48 +0100 blanchet tuning
Tue, 17 Dec 2013 14:22:42 +0100 blanchet removed workaround
Tue, 17 Dec 2013 14:15:23 +0100 blanchet tuning
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
Tue, 17 Dec 2013 11:12:10 +0100 immler NEWS
Tue, 17 Dec 2013 09:52:10 +0100 immler merged
Mon, 16 Dec 2013 17:08:22 +0100 immler lemmas about divideR and scaleR
Mon, 16 Dec 2013 17:08:22 +0100 immler monotonicity of rounding and truncating float
Mon, 16 Dec 2013 17:08:22 +0100 immler Float: prevent unnecessary large numbers when adding 0
Mon, 16 Dec 2013 17:08:22 +0100 immler additional definitions and lemmas for Float
Mon, 16 Dec 2013 17:08:22 +0100 immler additional lemmas
Mon, 16 Dec 2013 17:08:22 +0100 immler summarized notions related to ordered_euclidean_space and intervals in separate theory
Mon, 16 Dec 2013 17:08:22 +0100 immler pragmatic executability of instance prod::{open,dist,norm}
Mon, 16 Dec 2013 17:08:22 +0100 immler introduced ordered real vector spaces
Mon, 16 Dec 2013 17:08:22 +0100 immler remove redundant constants
Mon, 16 Dec 2013 17:08:22 +0100 immler ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
Mon, 16 Dec 2013 17:08:22 +0100 immler prefer box over greaterThanLessThan on euclidean_space
Tue, 17 Dec 2013 09:42:38 +0100 blanchet made SML/NJ happier
Mon, 16 Dec 2013 23:36:54 +0100 blanchet fixed source of 'Subscript' exception
Mon, 16 Dec 2013 23:05:16 +0100 blanchet handle Skolems gracefully for SPASS as well
Mon, 16 Dec 2013 20:43:04 +0100 blanchet move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
Mon, 16 Dec 2013 20:24:13 +0100 blanchet reverse Skolem function arguments
Mon, 16 Dec 2013 17:58:31 +0100 blanchet correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
Mon, 16 Dec 2013 17:18:52 +0100 blanchet fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
Mon, 16 Dec 2013 14:49:18 +0100 blanchet generalize method list further to list of list (clustering preferred methods together)
Mon, 16 Dec 2013 12:26:18 +0100 blanchet store alternative proof methods in Isar data structure
Mon, 16 Dec 2013 12:02:28 +0100 blanchet tuning
Mon, 16 Dec 2013 09:48:26 +0100 blanchet added 'meson' to the mix
Mon, 16 Dec 2013 09:40:02 +0100 blanchet tuning
Mon, 16 Dec 2013 09:17:58 +0100 blanchet made SML/NJ happy
Mon, 16 Dec 2013 08:35:03 +0100 blanchet use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
Sun, 15 Dec 2013 22:03:12 +0100 blanchet generate proper succedent for cases with trivial branches
Sun, 15 Dec 2013 20:31:25 +0100 blanchet tuning
Sun, 15 Dec 2013 20:09:13 +0100 blanchet simplify generated propositions
Sun, 15 Dec 2013 19:01:06 +0100 blanchet use 'prop' rather than 'bool' systematically in Isar reconstruction code
Sun, 15 Dec 2013 18:54:26 +0100 blanchet tuning
Sun, 15 Dec 2013 18:01:38 +0100 blanchet use 'arith' when appropriate in Z3 proofs
Sun, 15 Dec 2013 18:01:38 +0100 blanchet robustness in degenerate case + tuning
Sun, 15 Dec 2013 18:01:38 +0100 blanchet use simplifier for rewrite
Sun, 15 Dec 2013 18:01:38 +0100 blanchet more aggressive merging
Sun, 15 Dec 2013 18:01:38 +0100 blanchet implemented Z3 skolemization
Sun, 15 Dec 2013 18:01:38 +0100 blanchet inline Z3 hypotheses
Sun, 15 Dec 2013 18:01:35 +0100 blanchet merge
Sun, 15 Dec 2013 05:11:46 +0100 blanchet merge
Sat, 14 Dec 2013 07:45:30 +0800 blanchet merged
Sat, 14 Dec 2013 07:26:45 +0800 blanchet better handling of Z3 proof blocks
Sun, 15 Dec 2013 15:10:16 +0100 haftmann disambiguation of interpretation prefixes
Sun, 15 Dec 2013 15:10:14 +0100 haftmann more algebraic terminology for theories about big operators
Sat, 14 Dec 2013 20:46:36 +0100 wenzelm more antiquotations;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 13 Dec 2013 23:53:02 +0100 wenzelm merged
Fri, 13 Dec 2013 20:20:15 +0100 wenzelm maintain morphism names for diagnostic purposes;
Fri, 13 Dec 2013 14:58:47 +0100 wenzelm tuned -- prefer canonical argument order of fold_rev;
Fri, 13 Dec 2013 14:15:52 +0100 wenzelm proper simplifier context;
Fri, 13 Dec 2013 14:09:51 +0100 wenzelm tuned;
Fri, 13 Dec 2013 13:59:01 +0100 wenzelm tuned whitespace;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip