Wed, 30 Mar 2016 20:56:39 +0200 |
wenzelm |
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
|
changeset |
files
|
Wed, 30 Mar 2016 20:35:35 +0200 |
wenzelm |
avoid duplicate reports;
|
changeset |
files
|
Wed, 30 Mar 2016 19:31:28 +0200 |
wenzelm |
tuned messages -- position is usually missing here;
|
changeset |
files
|
Wed, 30 Mar 2016 19:25:04 +0200 |
wenzelm |
more PIDE markup;
|
changeset |
files
|
Wed, 30 Mar 2016 17:03:26 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
Wed, 30 Mar 2016 16:36:23 +0200 |
wenzelm |
clarified errors: more positions;
|
changeset |
files
|
Wed, 30 Mar 2016 15:15:12 +0200 |
wenzelm |
clarified simple mixfix;
|
changeset |
files
|
Wed, 30 Mar 2016 14:59:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 30 Mar 2016 14:52:23 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
Wed, 30 Mar 2016 14:35:41 +0200 |
wenzelm |
updated dependencies;
|
changeset |
files
|
Wed, 30 Mar 2016 14:33:40 +0200 |
wenzelm |
updated to Navigator 2.6;
|
changeset |
files
|
Wed, 30 Mar 2016 15:16:50 +0200 |
blanchet |
more 'corec' docs
|
changeset |
files
|
Tue, 29 Mar 2016 23:45:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
Tue, 29 Mar 2016 23:41:28 +0200 |
wenzelm |
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
|
changeset |
files
|
Tue, 29 Mar 2016 22:22:12 +0200 |
wenzelm |
tuned messages -- more positions;
|
changeset |
files
|
Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
changeset |
files
|
Tue, 29 Mar 2016 20:53:52 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
Tue, 29 Mar 2016 20:52:19 +0200 |
wenzelm |
proper norm_props, e.g. relevant for ML pp;
|
changeset |
files
|
Tue, 29 Mar 2016 16:20:48 +0200 |
wenzelm |
clarified reports;
|
changeset |
files
|
Tue, 29 Mar 2016 14:03:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
Tue, 29 Mar 2016 21:25:19 +0200 |
blanchet |
more 'corec' docs
|
changeset |
files
|
Tue, 29 Mar 2016 19:17:05 +0200 |
blanchet |
tuning
|
changeset |
files
|
Tue, 29 Mar 2016 19:11:03 +0200 |
blanchet |
more 'corec' docs
|
changeset |
files
|
Tue, 29 Mar 2016 18:32:08 +0200 |
blanchet |
try tactics in right order w.r.t. schematics
|
changeset |
files
|
Tue, 29 Mar 2016 18:07:55 +0200 |
blanchet |
more natural order for 'cong_intros'
|
changeset |
files
|
Tue, 29 Mar 2016 17:42:43 +0200 |
blanchet |
more 'corec' documentation
|
changeset |
files
|
Tue, 29 Mar 2016 10:57:02 +0200 |
blanchet |
renamed generated theorem
|
changeset |
files
|
Tue, 29 Mar 2016 09:49:39 +0200 |
blanchet |
tuning
|
changeset |
files
|
Tue, 29 Mar 2016 09:45:54 +0200 |
blanchet |
added sketchy 'corec' documentation
|
changeset |
files
|
Mon, 28 Mar 2016 12:11:54 +0200 |
blanchet |
compile
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
updated Sledgehammer documentation
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
a more generous hard timeout
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
another 'corec' example
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
don't ask too much of 'transfer_prover'
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
commented out for now
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
FIXME
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
avoid 'prove_sorry' for unreliable tactics
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
reused code
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuned examples
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
new 'corec' example
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
more reliable check for rhs variables
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
strengthened tactic
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML function
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
added '_legacy' suffixes
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML interface
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
changeset |
files
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
refined experimental option of Sledgehammer
|
changeset |
files
|
Sat, 26 Mar 2016 18:51:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 26 Mar 2016 16:14:46 +0100 |
wenzelm |
explicit print_depth for the sake of Spec_Check.determine_type;
|
changeset |
files
|
Sat, 26 Mar 2016 14:27:58 +0100 |
wenzelm |
obsolete -- done in Isabelle_Process.init_options;
|
changeset |
files
|
Sat, 26 Mar 2016 14:14:23 +0100 |
wenzelm |
clarified use of options;
|
changeset |
files
|
Sat, 26 Mar 2016 13:41:14 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
Sat, 26 Mar 2016 12:35:11 +0100 |
wenzelm |
clarified use of options;
|
changeset |
files
|
Sat, 26 Mar 2016 12:22:15 +0100 |
wenzelm |
avoid hardwired values;
|
changeset |
files
|
Sat, 26 Mar 2016 12:17:02 +0100 |
wenzelm |
eliminated duplicate;
|
changeset |
files
|
Sat, 26 Mar 2016 12:12:13 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
Thu, 24 Mar 2016 16:10:18 +0100 |
nipkow |
merged
|
changeset |
files
|