| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
prefer abstract simp rule
|
changeset |
files
|
| Wed, 25 Dec 2013 10:09:43 +0100 |
haftmann |
more lemmas on abstract lattices
|
changeset |
files
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
changeset |
files
|
| Tue, 24 Dec 2013 11:24:14 +0100 |
haftmann |
more general induction rule;
|
changeset |
files
|
| Mon, 23 Dec 2013 20:45:33 +0100 |
haftmann |
convenient printing of polynomial values
|
changeset |
files
|
| Mon, 23 Dec 2013 18:37:51 +0100 |
haftmann |
prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
|
changeset |
files
|
| Mon, 23 Dec 2013 16:29:43 +0100 |
haftmann |
prefer Y_of_X over X_to_Y;
|
changeset |
files
|
| Mon, 23 Dec 2013 16:59:56 +0100 |
panny |
merge
|
changeset |
files
|
| Mon, 23 Dec 2013 15:30:31 +0100 |
panny |
prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
|
changeset |
files
|
| Mon, 23 Dec 2013 16:16:36 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Mon, 23 Dec 2013 14:24:22 +0100 |
haftmann |
dropped redundant lemma
|
changeset |
files
|
| Mon, 23 Dec 2013 14:24:21 +0100 |
haftmann |
syntactically tuned
|
changeset |
files
|
| Mon, 23 Dec 2013 14:24:20 +0100 |
haftmann |
prefer plain bool over dedicated type for binary digits
|
changeset |
files
|
| Mon, 23 Dec 2013 09:21:38 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sat, 21 Dec 2013 09:44:30 +0100 |
blanchet |
compile + reduce problem size by a notch
|
changeset |
files
|
| Sat, 21 Dec 2013 09:44:30 +0100 |
blanchet |
generate exhaust from nchotomy
|
changeset |
files
|
| Sat, 21 Dec 2013 09:44:29 +0100 |
blanchet |
made tactic work with theorems with multiple assumptions
|
changeset |
files
|
| Sat, 21 Dec 2013 09:44:28 +0100 |
blanchet |
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
|
changeset |
files
|
| Wed, 18 Dec 2013 11:03:40 +0100 |
traytel |
express weak pullback property of bnfs only in terms of the relator
|
changeset |
files
|
| Fri, 20 Dec 2013 21:09:01 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 20 Dec 2013 21:08:48 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 20 Dec 2013 20:36:38 +0100 |
blanchet |
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
|
changeset |
files
|
| Fri, 20 Dec 2013 16:22:10 +0100 |
blanchet |
tuning whitespace
|
changeset |
files
|
| Fri, 20 Dec 2013 14:27:07 +0100 |
blanchet |
recognize datatype reasoning in SPASS-Pirate
|
changeset |
files
|
| Fri, 20 Dec 2013 11:34:07 +0100 |
blanchet |
note manually proved exclusiveness property
|
changeset |
files
|
| Fri, 20 Dec 2013 11:12:51 +0100 |
blanchet |
note exhaust proof obligation
|
changeset |
files
|
| Fri, 20 Dec 2013 09:48:04 +0100 |
blanchet |
compile
|
changeset |
files
|
| Thu, 19 Dec 2013 21:49:30 +0100 |
blanchet |
implemented 'exhaustive' option in tactic
|
changeset |
files
|
| Thu, 19 Dec 2013 20:07:06 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 19 Dec 2013 19:37:43 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 19 Dec 2013 19:35:50 +0100 |
blanchet |
tuning 'case' expressions
|
changeset |
files
|
| Thu, 19 Dec 2013 19:16:44 +0100 |
blanchet |
don't do 'isar_try0' if preplaying is off
|
changeset |
files
|
| Thu, 19 Dec 2013 18:39:54 +0100 |
blanchet |
more data structure refactoring
|
changeset |
files
|
| Thu, 19 Dec 2013 18:22:31 +0100 |
blanchet |
data structure rationalization
|
changeset |
files
|
| Thu, 19 Dec 2013 18:07:21 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 19 Dec 2013 17:52:58 +0100 |
blanchet |
refactored preplaying outcome data structure
|
changeset |
files
|
| Thu, 19 Dec 2013 17:24:17 +0100 |
blanchet |
distinguish not preplayed & timed out
|
changeset |
files
|
| Thu, 19 Dec 2013 17:11:54 +0100 |
blanchet |
pick up tfree/tvar type from SPASS-Pirate proof
|
changeset |
files
|
| Thu, 19 Dec 2013 16:11:20 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 19 Dec 2013 15:47:17 +0100 |
blanchet |
extended ATP types with sorts
|
changeset |
files
|
| Thu, 19 Dec 2013 15:04:21 +0100 |
blanchet |
removed debugging output
|
changeset |
files
|
| Thu, 19 Dec 2013 14:57:21 +0100 |
blanchet |
honor SPASS-Pirate type arguments
|
changeset |
files
|
| Thu, 19 Dec 2013 13:46:42 +0100 |
blanchet |
made SML/NJ-friendlier (hopefully)
|
changeset |
files
|
| Thu, 19 Dec 2013 13:43:21 +0100 |
blanchet |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
changeset |
files
|
| Thu, 19 Dec 2013 10:15:12 +0100 |
blanchet |
simplified data structure
|
changeset |
files
|
| Thu, 19 Dec 2013 10:12:28 +0100 |
blanchet |
prevent curl's output to interfere with the prover's output
|
changeset |
files
|
| Thu, 19 Dec 2013 09:28:20 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 18 Dec 2013 22:55:43 +0100 |
blanchet |
merge
|
changeset |
files
|
| Wed, 18 Dec 2013 22:55:20 +0100 |
blanchet |
parse SPASS-Pirate types
|
changeset |
files
|
| Wed, 18 Dec 2013 17:52:52 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 18 Dec 2013 17:52:44 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 18 Dec 2013 17:48:48 +0100 |
panny |
merge
|
changeset |
files
|
| Wed, 18 Dec 2013 14:50:25 +0100 |
panny |
pass down user input in more cases in order to preserve "let"s etc.
|
changeset |
files
|
| Wed, 18 Dec 2013 14:06:34 +0100 |
panny |
pass auto-proved exhaustiveness properties to tactic;
|
changeset |
files
|
| Wed, 18 Dec 2013 17:27:17 +0100 |
blanchet |
merge
|
changeset |
files
|
| Wed, 18 Dec 2013 17:26:31 +0100 |
blanchet |
changed pirate port
|
changeset |
files
|
| Wed, 18 Dec 2013 17:00:14 +0100 |
blanchet |
fixed variable confusion introduced by 'tuning' change 565f9af86d67
|
changeset |
files
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
try 'auto' first -- more likely to succeed
|
changeset |
files
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
new port
|
changeset |
files
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
generate type classes for tfrees
|
changeset |
files
|
| Wed, 18 Dec 2013 11:53:40 +0100 |
hoelzl |
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
|
changeset |
files
|
| Tue, 17 Dec 2013 22:34:26 +0100 |
haftmann |
avoid clashes of fact names
|
changeset |
files
|
| 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
|
changeset |
files
|
| Tue, 17 Dec 2013 15:56:57 +0100 |
traytel |
reduced cardinals dependencies of (co)datatypes
|
changeset |
files
|
| Tue, 17 Dec 2013 15:44:10 +0100 |
traytel |
tighter bnf bounds for (co)datatypes
|
changeset |
files
|
| Tue, 17 Dec 2013 15:15:59 +0100 |
traytel |
tuned
|
changeset |
files
|
| Tue, 17 Dec 2013 14:22:48 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 17 Dec 2013 14:22:42 +0100 |
blanchet |
removed workaround
|
changeset |
files
|
| Tue, 17 Dec 2013 14:15:23 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 17 Dec 2013 14:03:29 +0100 |
blanchet |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
changeset |
files
|
| Tue, 17 Dec 2013 11:12:10 +0100 |
immler |
NEWS
|
changeset |
files
|
| Tue, 17 Dec 2013 09:52:10 +0100 |
immler |
merged
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
lemmas about divideR and scaleR
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
monotonicity of rounding and truncating float
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
Float: prevent unnecessary large numbers when adding 0
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional definitions and lemmas for Float
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional lemmas
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
summarized notions related to ordered_euclidean_space and intervals in separate theory
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
pragmatic executability of instance prod::{open,dist,norm}
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
introduced ordered real vector spaces
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
remove redundant constants
|
changeset |
files
|
| 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
|
changeset |
files
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
changeset |
files
|
| Tue, 17 Dec 2013 09:42:38 +0100 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Mon, 16 Dec 2013 23:36:54 +0100 |
blanchet |
fixed source of 'Subscript' exception
|
changeset |
files
|
| Mon, 16 Dec 2013 23:05:16 +0100 |
blanchet |
handle Skolems gracefully for SPASS as well
|
changeset |
files
|
| 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)
|
changeset |
files
|
| Mon, 16 Dec 2013 20:24:13 +0100 |
blanchet |
reverse Skolem function arguments
|
changeset |
files
|
| Mon, 16 Dec 2013 17:58:31 +0100 |
blanchet |
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
|
changeset |
files
|
| Mon, 16 Dec 2013 17:18:52 +0100 |
blanchet |
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
|
changeset |
files
|
| Mon, 16 Dec 2013 14:49:18 +0100 |
blanchet |
generalize method list further to list of list (clustering preferred methods together)
|
changeset |
files
|
| Mon, 16 Dec 2013 12:26:18 +0100 |
blanchet |
store alternative proof methods in Isar data structure
|
changeset |
files
|
| Mon, 16 Dec 2013 12:02:28 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 16 Dec 2013 09:48:26 +0100 |
blanchet |
added 'meson' to the mix
|
changeset |
files
|
| Mon, 16 Dec 2013 09:40:02 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 16 Dec 2013 09:17:58 +0100 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Mon, 16 Dec 2013 08:35:03 +0100 |
blanchet |
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 22:03:12 +0100 |
blanchet |
generate proper succedent for cases with trivial branches
|
changeset |
files
|
| Sun, 15 Dec 2013 20:31:25 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 20:09:13 +0100 |
blanchet |
simplify generated propositions
|
changeset |
files
|
| Sun, 15 Dec 2013 19:01:06 +0100 |
blanchet |
use 'prop' rather than 'bool' systematically in Isar reconstruction code
|
changeset |
files
|
| Sun, 15 Dec 2013 18:54:26 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
use 'arith' when appropriate in Z3 proofs
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
robustness in degenerate case + tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
use simplifier for rewrite
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
more aggressive merging
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
implemented Z3 skolemization
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
inline Z3 hypotheses
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:35 +0100 |
blanchet |
merge
|
changeset |
files
|
| Sun, 15 Dec 2013 05:11:46 +0100 |
blanchet |
merge
|
changeset |
files
|
| Sat, 14 Dec 2013 07:45:30 +0800 |
blanchet |
merged
|
changeset |
files
|
| Sat, 14 Dec 2013 07:26:45 +0800 |
blanchet |
better handling of Z3 proof blocks
|
changeset |
files
|
| Sun, 15 Dec 2013 15:10:16 +0100 |
haftmann |
disambiguation of interpretation prefixes
|
changeset |
files
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
changeset |
files
|
| Sat, 14 Dec 2013 20:46:36 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
changeset |
files
|
| Fri, 13 Dec 2013 23:53:02 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:58:47 +0100 |
wenzelm |
tuned -- prefer canonical argument order of fold_rev;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:15:52 +0100 |
wenzelm |
proper simplifier context;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:09:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 13 Dec 2013 13:59:01 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 13 Dec 2013 22:54:39 +0800 |
blanchet |
made SML/NJ happy + whitespace tuning
|
changeset |
files
|
| Fri, 13 Dec 2013 12:31:45 +0100 |
wenzelm |
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
|
changeset |
files
|
| Thu, 12 Dec 2013 23:18:47 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 12 Dec 2013 22:56:28 +0100 |
wenzelm |
discontinued legacy_isub_isup;
|
changeset |
files
|
| Thu, 12 Dec 2013 22:38:25 +0100 |
wenzelm |
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
|
changeset |
files
|
| Thu, 12 Dec 2013 21:28:13 +0100 |
wenzelm |
skeleton for Simplifier trace by Lars Hupel;
|
changeset |
files
|
| Thu, 12 Dec 2013 21:14:33 +0100 |
wenzelm |
generic trace operations for main steps of Simplifier;
|
changeset |
files
|
| Thu, 12 Dec 2013 17:34:50 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 12 Dec 2013 16:56:53 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 12 Dec 2013 16:25:21 +0100 |
wenzelm |
added missing file (cf. 124432e77ecf);
|
changeset |
files
|
| Thu, 12 Dec 2013 16:17:35 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 12 Dec 2013 14:35:31 +0100 |
wenzelm |
removed dead code -- ctxt is never visible (see also 658fcba35ed7);
|
changeset |
files
|
| Thu, 12 Dec 2013 13:50:44 +0100 |
wenzelm |
simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
|
changeset |
files
|
| Thu, 12 Dec 2013 13:23:23 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 12 Dec 2013 17:02:52 +0100 |
haftmann |
be more explicit about pre- and postprocessor, particularly code_abbrev
|
changeset |
files
|
| Wed, 11 Dec 2013 17:30:51 +0100 |
traytel |
removed obsolete codegen setup; Stream -> SCons; tuned
|
changeset |
files
|
| Wed, 11 Dec 2013 20:57:47 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 11 Dec 2013 20:38:39 +0100 |
wenzelm |
tuned patterns;
|
changeset |
files
|
| Wed, 11 Dec 2013 18:02:22 +0100 |
wenzelm |
support for polml-5.5.2;
|
changeset |
files
|
| Wed, 11 Dec 2013 22:53:32 +0800 |
blanchet |
reverse order in which lines are selected, to ensure that the number of dependencies is accurate
|
changeset |
files
|
| Wed, 11 Dec 2013 22:23:42 +0800 |
blanchet |
truncate proof once False is hit to avoid confusing the rest of the code (no idea why Z3 goes on)
|
changeset |
files
|
| Wed, 11 Dec 2013 22:23:07 +0800 |
blanchet |
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
|
changeset |
files
|
| Wed, 11 Dec 2013 00:17:09 +0000 |
paulson |
Fib: Who needs the int version?
|
changeset |
files
|
| Tue, 10 Dec 2013 15:24:17 +0800 |
blanchet |
more work on Z3 Isar proofs
|
changeset |
files
|
| Mon, 09 Dec 2013 23:22:44 +0000 |
paulson |
streamlined two proofs
|
changeset |
files
|
| Mon, 09 Dec 2013 23:16:10 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 09 Dec 2013 22:02:42 +0100 |
wenzelm |
alternative hires icon;
|
changeset |
files
|
| Mon, 09 Dec 2013 22:49:27 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Sat, 07 Dec 2013 20:09:35 +0100 |
haftmann |
default code equations for make, fields, extend and truncate operations on records
|
changeset |
files
|
| Mon, 09 Dec 2013 21:32:45 +0100 |
wenzelm |
browse directory hyperlink as well;
|
changeset |
files
|
| Mon, 09 Dec 2013 20:16:12 +0100 |
wenzelm |
provide @{file_unchecked} in Isabelle/Pure;
|
changeset |
files
|
| Mon, 09 Dec 2013 12:27:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 09 Dec 2013 12:22:23 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Mon, 09 Dec 2013 12:16:52 +0100 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
changeset |
files
|
| Mon, 09 Dec 2013 09:44:57 +0100 |
blanchet |
tuning -- moved ML files to subdirectory
|
changeset |
files
|
| Mon, 09 Dec 2013 06:33:46 +0100 |
blanchet |
adapted code for Z3 proof reconstruction
|
changeset |
files
|
| Mon, 09 Dec 2013 05:06:48 +0100 |
blanchet |
useful debugging info
|
changeset |
files
|
| Mon, 09 Dec 2013 04:44:59 +0100 |
blanchet |
disable generalization in MaSh until it is shown to help
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
bugfixes to Python MaSh related to alternative features
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
compile
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
generate problems with type classes
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
added warning to documentation, based on isabelle-users thread
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
more reasonable default weight
|
changeset |
files
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
added multiple feature capability to MaSh
|
changeset |
files
|
| Sat, 07 Dec 2013 18:06:49 +0100 |
traytel |
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
|
changeset |
files
|
| Sat, 07 Dec 2013 13:10:56 +0100 |
wenzelm |
more direct Isabelle_System.pdf_viewer;
|
changeset |
files
|
| Sat, 07 Dec 2013 12:52:31 +0100 |
wenzelm |
proper latex;
|
changeset |
files
|
| Fri, 06 Dec 2013 23:36:28 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Fri, 06 Dec 2013 23:34:14 +0100 |
wenzelm |
no keyboard control -- avoid confusion about meaning of selection;
|
changeset |
files
|
| Fri, 06 Dec 2013 23:25:38 +0100 |
wenzelm |
directly react on click, assuming that document view operation is mostly idempotent;
|
changeset |
files
|
| Fri, 06 Dec 2013 22:50:47 +0100 |
wenzelm |
generic $ISABELLE_OPEN;
|
changeset |
files
|
| Fri, 06 Dec 2013 22:35:51 +0100 |
wenzelm |
updated to Sumatra PDF 2.4;
|
changeset |
files
|
| Fri, 06 Dec 2013 22:10:45 +0100 |
wenzelm |
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
|
changeset |
files
|
| Fri, 06 Dec 2013 21:49:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Dec 2013 17:33:45 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 06 Dec 2013 09:42:13 +0100 |
blanchet |
reverted 86e0b402994c, which was accidentally qfinish'ed and pushed
|
changeset |
files
|
| Thu, 05 Dec 2013 23:13:54 +0000 |
paulson |
Better simprules and markup. Restored the natural number version of the binomial theorem
|
changeset |
files
|
| Thu, 05 Dec 2013 20:22:53 +0100 |
wenzelm |
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
|
changeset |
files
|
| Thu, 05 Dec 2013 20:06:28 +0100 |
wenzelm |
strict EXEC_PROCESS: component can be expected to be present;
|
changeset |
files
|
| Thu, 05 Dec 2013 19:59:43 +0100 |
wenzelm |
uniform use of transparent icons, as for main "apps";
|
changeset |
files
|
| Thu, 05 Dec 2013 19:47:48 +0100 |
wenzelm |
more isabelle logos (from isabelle_transparent.ico);
|
changeset |
files
|
| Thu, 05 Dec 2013 18:28:06 +0100 |
wenzelm |
recover 175b43e0b9ce from lost update in cc126144f662;
|
changeset |
files
|
| Thu, 05 Dec 2013 18:25:28 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 05 Dec 2013 18:02:55 +0100 |
wenzelm |
relocate NEWS to post-release version (cf. 7a14f831d02d);
|
changeset |
files
|
| Thu, 05 Dec 2013 17:58:03 +0100 |
wenzelm |
merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
|
changeset |
files
|
| Thu, 05 Dec 2013 17:52:12 +0100 |
wenzelm |
removed obsolete RC tags;
|
changeset |
files
|
| Thu, 05 Dec 2013 17:51:29 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Thu, 05 Dec 2013 16:14:50 +0100 |
wenzelm |
Added tag Isabelle2013-2 for changeset 4dd08fe126ba
|
changeset |
files
|
| Wed, 04 Dec 2013 18:59:20 +0100 |
wenzelm |
remove junk;
Isabelle2013-2
|
changeset |
files
|
| Wed, 04 Dec 2013 18:38:26 +0100 |
wenzelm |
recover main entry point from d9c88171b393 -- occasionally useful with plain "java -jar jedit.jar";
|
changeset |
files
|
| Mon, 02 Dec 2013 15:49:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Dec 2013 17:09:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Dec 2013 16:35:38 +0100 |
wenzelm |
Added tag Isabelle2013-2-RC3 for changeset aeb21314d078
|
changeset |
files
|
| Sun, 01 Dec 2013 16:01:03 +0100 |
wenzelm |
prefer transparent application icon (like Mac OS X);
|
changeset |
files
|
| Sun, 01 Dec 2013 14:09:33 +0100 |
wenzelm |
specific application name for official bundle (as for Mac OS X);
|
changeset |
files
|
| Sun, 01 Dec 2013 13:54:41 +0100 |
wenzelm |
prefer isabelle application icon;
|
changeset |
files
|
| Sun, 01 Dec 2013 13:03:15 +0100 |
wenzelm |
more isabelle logos (from isabelle.ico);
|
changeset |
files
|
| Sat, 30 Nov 2013 22:56:20 +0100 |
wenzelm |
prefer 32x32 icon like jedit (image from isabelle.ico);
|
changeset |
files
|
| Sat, 30 Nov 2013 21:17:53 +0100 |
wenzelm |
updated isabelle.ico for the record (see also 84177f8372f9);
|
changeset |
files
|
| Sat, 30 Nov 2013 20:59:12 +0100 |
wenzelm |
updated icon of Isabelle.exe, using http://convertico.org/image_to_icon_converter on lib/logo/isabelle.gif (approx. 256x256 pixels according to Windows 7 format);
|
changeset |
files
|
| Sat, 30 Nov 2013 17:51:25 +0100 |
wenzelm |
further encouragement to read jEdit documentation;
|
changeset |
files
|
| Sat, 30 Nov 2013 17:38:08 +0100 |
wenzelm |
clarified view.title;
|
changeset |
files
|
| Sat, 30 Nov 2013 17:26:00 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sat, 30 Nov 2013 16:07:00 +0100 |
wenzelm |
non-focusable button, to avoid second interpretation of SPACE in C+e SPACE (isabelle.set-node-required);
|
changeset |
files
|
| Sat, 30 Nov 2013 15:05:10 +0100 |
wenzelm |
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
|
changeset |
files
|
| Thu, 28 Nov 2013 13:59:00 +0100 |
wenzelm |
Added tag Isabelle2013-2-RC2 for changeset 99b9249b3e05
|
changeset |
files
|
| Thu, 28 Nov 2013 12:54:39 +0100 |
wenzelm |
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
|
changeset |
files
|
| Mon, 25 Nov 2013 21:36:10 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 25 Nov 2013 21:17:18 +0100 |
wenzelm |
more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;
|
changeset |
files
|
| Mon, 25 Nov 2013 20:49:20 +0100 |
wenzelm |
more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
|
changeset |
files
|
| Mon, 25 Nov 2013 18:03:38 +0100 |
wenzelm |
more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
|
changeset |
files
|
| Sun, 24 Nov 2013 18:06:09 +0100 |
wenzelm |
Added tag Isabelle2013-2-RC1 for changeset 57aefb80b639
|
changeset |
files
|
| Sat, 23 Nov 2013 12:59:12 +0100 |
wenzelm |
more on GTK;
|
changeset |
files
|
| Fri, 22 Nov 2013 21:57:50 +0100 |
wenzelm |
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798 (clone of f6ffe53387ef);
|
changeset |
files
|
| Thu, 21 Nov 2013 22:13:11 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Thu, 21 Nov 2013 21:55:29 +0100 |
wenzelm |
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
|
changeset |
files
|
| Wed, 20 Nov 2013 23:00:18 +0100 |
wenzelm |
updated to Isabelle2013-2;
|
changeset |
files
|
| Wed, 20 Nov 2013 22:15:53 +0100 |
wenzelm |
compile on Windows (clone of d04576557400);
|
changeset |
files
|
| Wed, 20 Nov 2013 22:10:45 +0100 |
wenzelm |
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
|
changeset |
files
|
| Thu, 05 Dec 2013 17:09:13 +0000 |
paulson |
updated mirror script for Cambridge
|
changeset |
files
|
| Thu, 05 Dec 2013 14:35:58 +0100 |
blanchet |
proper code generation for discriminators/selectors
|
changeset |
files
|
| Thu, 05 Dec 2013 14:11:45 +0100 |
blanchet |
reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
|
changeset |
files
|
| Thu, 05 Dec 2013 13:38:20 +0100 |
blanchet |
experiment
|
changeset |
files
|
| Thu, 05 Dec 2013 13:22:00 +0100 |
blanchet |
make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
|
changeset |
files
|
| Thu, 05 Dec 2013 09:23:59 +0100 |
Andreas Lochbihler |
news
|
changeset |
files
|
| Thu, 05 Dec 2013 09:20:32 +0100 |
Andreas Lochbihler |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
changeset |
files
|
| Tue, 03 Dec 2013 02:51:20 +0100 |
panny |
merge
|
changeset |
files
|
| Mon, 02 Dec 2013 19:49:34 +0100 |
panny |
generate "code" theorems for incomplete definitions
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
updated keywords
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
added 'no_code' option
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
killed obsolete artifact
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
avoid user-level 'Specification.definition' for low-level definitions
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
repaired inconsistency introduced in transiting to 'Local_Theory.define'
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
docs for forgotten BNF theorems
|
changeset |
files
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
tuning
|
changeset |
files
|