immler [Tue, 17 Dec 2013 11:12:10 +0100] rev 54787
NEWS
immler [Tue, 17 Dec 2013 09:52:10 +0100] rev 54786
merged
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54785
lemmas about divideR and scaleR
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54784
monotonicity of rounding and truncating float
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54783
Float: prevent unnecessary large numbers when adding 0
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54782
additional definitions and lemmas for Float
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54781
additional lemmas
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54780
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54779
pragmatic executability of instance prod::{open,dist,norm}
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54778
introduced ordered real vector spaces
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54777
remove redundant constants
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54776
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler [Mon, 16 Dec 2013 17:08:22 +0100] rev 54775
prefer box over greaterThanLessThan on euclidean_space
blanchet [Tue, 17 Dec 2013 09:42:38 +0100] rev 54774
made SML/NJ happier
blanchet [Mon, 16 Dec 2013 23:36:54 +0100] rev 54773
fixed source of 'Subscript' exception
blanchet [Mon, 16 Dec 2013 23:05:16 +0100] rev 54772
handle Skolems gracefully for SPASS as well
blanchet [Mon, 16 Dec 2013 20:43:04 +0100] rev 54771
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet [Mon, 16 Dec 2013 20:24:13 +0100] rev 54770
reverse Skolem function arguments
blanchet [Mon, 16 Dec 2013 17:58:31 +0100] rev 54769
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet [Mon, 16 Dec 2013 17:18:52 +0100] rev 54768
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet [Mon, 16 Dec 2013 14:49:18 +0100] rev 54767
generalize method list further to list of list (clustering preferred methods together)
blanchet [Mon, 16 Dec 2013 12:26:18 +0100] rev 54766
store alternative proof methods in Isar data structure
blanchet [Mon, 16 Dec 2013 12:02:28 +0100] rev 54765
tuning
blanchet [Mon, 16 Dec 2013 09:48:26 +0100] rev 54764
added 'meson' to the mix
blanchet [Mon, 16 Dec 2013 09:40:02 +0100] rev 54763
tuning
blanchet [Mon, 16 Dec 2013 09:17:58 +0100] rev 54762
made SML/NJ happy
blanchet [Mon, 16 Dec 2013 08:35:03 +0100] rev 54761
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet [Sun, 15 Dec 2013 22:03:12 +0100] rev 54760
generate proper succedent for cases with trivial branches
blanchet [Sun, 15 Dec 2013 20:31:25 +0100] rev 54759
tuning
blanchet [Sun, 15 Dec 2013 20:09:13 +0100] rev 54758
simplify generated propositions
blanchet [Sun, 15 Dec 2013 19:01:06 +0100] rev 54757
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet [Sun, 15 Dec 2013 18:54:26 +0100] rev 54756
tuning
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54755
use 'arith' when appropriate in Z3 proofs
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54754
robustness in degenerate case + tuning
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54753
use simplifier for rewrite
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54752
more aggressive merging
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54751
implemented Z3 skolemization
blanchet [Sun, 15 Dec 2013 18:01:38 +0100] rev 54750
inline Z3 hypotheses
blanchet [Sun, 15 Dec 2013 18:01:35 +0100] rev 54749
merge
blanchet [Sun, 15 Dec 2013 05:11:46 +0100] rev 54748
merge
blanchet [Sat, 14 Dec 2013 07:45:30 +0800] rev 54747
merged
blanchet [Sat, 14 Dec 2013 07:26:45 +0800] rev 54746
better handling of Z3 proof blocks
haftmann [Sun, 15 Dec 2013 15:10:16 +0100] rev 54745
disambiguation of interpretation prefixes
haftmann [Sun, 15 Dec 2013 15:10:14 +0100] rev 54744
more algebraic terminology for theories about big operators
wenzelm [Sat, 14 Dec 2013 20:46:36 +0100] rev 54743
more antiquotations;
wenzelm [Sat, 14 Dec 2013 17:28:05 +0100] rev 54742
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
wenzelm [Fri, 13 Dec 2013 23:53:02 +0100] rev 54741
merged
wenzelm [Fri, 13 Dec 2013 20:20:15 +0100] rev 54740
maintain morphism names for diagnostic purposes;
wenzelm [Fri, 13 Dec 2013 14:58:47 +0100] rev 54739
tuned -- prefer canonical argument order of fold_rev;
wenzelm [Fri, 13 Dec 2013 14:15:52 +0100] rev 54738
proper simplifier context;
more standard "cert";
wenzelm [Fri, 13 Dec 2013 14:09:51 +0100] rev 54737
tuned;
wenzelm [Fri, 13 Dec 2013 13:59:01 +0100] rev 54736
tuned whitespace;
blanchet [Fri, 13 Dec 2013 22:54:39 +0800] rev 54735
made SML/NJ happy + whitespace tuning
wenzelm [Fri, 13 Dec 2013 12:31:45 +0100] rev 54734
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
wenzelm [Thu, 12 Dec 2013 23:18:47 +0100] rev 54733
merged
wenzelm [Thu, 12 Dec 2013 22:56:28 +0100] rev 54732
discontinued legacy_isub_isup;
wenzelm [Thu, 12 Dec 2013 22:38:25 +0100] rev 54731
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm [Thu, 12 Dec 2013 21:28:13 +0100] rev 54730
skeleton for Simplifier trace by Lars Hupel;
wenzelm [Thu, 12 Dec 2013 21:14:33 +0100] rev 54729
generic trace operations for main steps of Simplifier;
wenzelm [Thu, 12 Dec 2013 17:34:50 +0100] rev 54728
tuned signature;