| Fri, 14 Nov 2014 08:18:58 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
changeset |
files
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
changeset |
files
|
| Thu, 13 Nov 2014 17:28:11 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 13 Nov 2014 14:40:06 +0100 |
traytel |
merged
|
changeset |
files
|
| Thu, 13 Nov 2014 14:14:13 +0100 |
traytel |
do not introduce consts too early unnecessarily
|
changeset |
files
|
| Thu, 13 Nov 2014 12:35:55 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 12 Nov 2014 19:30:56 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 Nov 2014 18:18:38 +0100 |
wenzelm |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
changeset |
files
|
| Wed, 12 Nov 2014 11:39:27 +0100 |
wenzelm |
make SML/NJ happy;
|
changeset |
files
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:44 +0100 |
immler |
NEWS
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
tuned proofs
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
added quickcheck[approximation]
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
disjunction and conjunction for forms
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
truncate intermediate results in horner to improve performance of approximate;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:36 +0100 |
immler |
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:32 +0100 |
immler |
cancel real of power of numeral also for equality and strict inequality;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:29 +0100 |
immler |
simplified computations based on round_up by reducing to round_down;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:25 +0100 |
immler |
code equation for powr
|
changeset |
files
|
| Tue, 11 Nov 2014 21:14:19 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
changeset |
files
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
changeset |
files
|
| Tue, 11 Nov 2014 15:55:31 +0100 |
wenzelm |
more symbols;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:50:56 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:44:09 +0100 |
wenzelm |
more markup;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:40:13 +0100 |
wenzelm |
simplifie sessions;
|
changeset |
files
|
| Tue, 11 Nov 2014 11:47:53 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 11:41:58 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 10:54:52 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 19:38:45 +0100 |
noschinl |
add forgotten lemma
|
changeset |
files
|
| Tue, 11 Nov 2014 14:46:26 +0100 |
noschinl |
added lemma
|
changeset |
files
|
| Tue, 11 Nov 2014 12:30:37 +0100 |
desharna |
make 'corec_transfer' tactic more robust
|
changeset |
files
|
| Tue, 11 Nov 2014 12:30:36 +0100 |
desharna |
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
|
changeset |
files
|
| Tue, 11 Nov 2014 10:26:08 +0100 |
desharna |
make 'rec_transfer' tactic more robust
|
changeset |
files
|
| Tue, 11 Nov 2014 08:57:46 +0100 |
Andreas Lochbihler |
add del option to measurable;
|
changeset |
files
|
| Tue, 11 Nov 2014 00:11:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
changeset |
files
|
| Mon, 10 Nov 2014 15:09:58 +0100 |
nipkow |
even -> evn because even is now in Main
|
changeset |
files
|
| Mon, 10 Nov 2014 10:29:19 +0100 |
traytel |
dropped redundant transfer rules (now proved and registered by datatype and plugins)
|
changeset |
files
|
| Sun, 09 Nov 2014 20:49:28 +0100 |
wenzelm |
proper context for typedef;
|
changeset |
files
|
| Sun, 09 Nov 2014 20:41:53 +0100 |
wenzelm |
proper proof context for typedef;
|
changeset |
files
|
| Sun, 09 Nov 2014 18:27:43 +0100 |
wenzelm |
proper context;
|
changeset |
files
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
changeset |
files
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
changeset |
files
|
| Sun, 09 Nov 2014 11:05:20 +0100 |
nipkow |
avoid erule and rotated in IMP
|
changeset |
files
|
| Sun, 09 Nov 2014 10:03:18 +0100 |
haftmann |
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
|
changeset |
files
|
| Sun, 09 Nov 2014 10:03:17 +0100 |
haftmann |
self-contained simp rules for dvd on numerals
|
changeset |
files
|
| Sat, 08 Nov 2014 16:53:26 +0100 |
haftmann |
equivalence rules for structures without zero divisors
|
changeset |
files
|
| Sat, 08 Nov 2014 22:10:16 +0100 |
wenzelm |
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
|
changeset |
files
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
changeset |
files
|
| Sat, 08 Nov 2014 17:39:01 +0100 |
wenzelm |
clarified name of Type.unified, to emphasize its connection to the "unify" family;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:55:41 +0100 |
wenzelm |
proper Envir.norm_type for result of Type.raw_unifys;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:42:04 +0100 |
wenzelm |
avoid slow metis proof;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:35:24 +0100 |
wenzelm |
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
|
changeset |
files
|
| Sat, 08 Nov 2014 15:45:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 08 Nov 2014 15:44:41 +0100 |
wenzelm |
updated some sledgehammer proofs -- much faster;
|
changeset |
files
|
| Sat, 08 Nov 2014 15:40:29 +0100 |
wenzelm |
updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);
|
changeset |
files
|
| Sat, 08 Nov 2014 15:01:05 +0100 |
wenzelm |
recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
|
changeset |
files
|
| Sat, 08 Nov 2014 12:15:40 +0100 |
wenzelm |
more direct type equality;
|
changeset |
files
|
| Sat, 08 Nov 2014 09:19:57 +0100 |
haftmann |
reverted commit accident from 994fe0ba8335
|
changeset |
files
|
| Sat, 08 Nov 2014 09:16:47 +0100 |
haftmann |
less space-wasting serialization setup: highest cell of array has been unused so far
|
changeset |
files
|
| Fri, 07 Nov 2014 23:35:13 +0100 |
wenzelm |
tuned outline;
|
changeset |
files
|
| Fri, 07 Nov 2014 22:33:54 +0100 |
wenzelm |
tuned syntax -- separate tokens;
|
changeset |
files
|
| Fri, 07 Nov 2014 22:15:51 +0100 |
wenzelm |
eliminated pointless check -- command definitions are subject to theory context;
|
changeset |
files
|
| Fri, 07 Nov 2014 20:43:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 07 Nov 2014 20:06:18 +0100 |
wenzelm |
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
|
changeset |
files
|
| Fri, 07 Nov 2014 19:47:05 +0100 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Fri, 07 Nov 2014 17:43:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Nov 2014 17:31:01 +0100 |
wenzelm |
clarified keyword categories;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:55:09 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:51:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:22:25 +0100 |
wenzelm |
proper import for command 'permanent_interpretation';
|
changeset |
files
|
| Fri, 07 Nov 2014 16:13:05 +0100 |
wenzelm |
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
|
changeset |
files
|
| Fri, 07 Nov 2014 15:19:30 +0100 |
wenzelm |
more accurate keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 16:10:33 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Nov 2014 15:47:04 +0100 |
wenzelm |
more explicit Keyword.keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 15:42:34 +0100 |
wenzelm |
proper Keyword.keywords (cf. 82a71046dce8);
|
changeset |
files
|
| Thu, 06 Nov 2014 15:05:15 +0100 |
wenzelm |
prefer explicit Keyword.keywords (cf. 82a71046dce8);
|
changeset |
files
|
| Thu, 06 Nov 2014 13:44:14 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Nov 2014 13:36:19 +0100 |
wenzelm |
prefer explicit Keyword.keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
changeset |
files
|
| Fri, 07 Nov 2014 15:40:08 +0000 |
paulson |
Tidying up. Removing unnecessary conditions from some theorems.
|
changeset |
files
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
changeset |
files
|
| Fri, 07 Nov 2014 12:24:56 +0100 |
desharna |
document '*_transfer' attribute
|
changeset |
files
|
| Fri, 07 Nov 2014 11:52:56 +0100 |
desharna |
document 'size_neq'
|
changeset |
files
|
| Fri, 07 Nov 2014 11:52:54 +0100 |
desharna |
generate 'size_neq' for datatypes
|
changeset |
files
|
| Thu, 06 Nov 2014 15:21:59 +0100 |
desharna |
fix 'unfla' function
|
changeset |
files
|
| Wed, 05 Nov 2014 20:59:24 +0100 |
haftmann |
proper oriented equivalence of dvd predicate and mod
|
changeset |
files
|
| Wed, 05 Nov 2014 22:39:49 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 05 Nov 2014 22:37:14 +0100 |
wenzelm |
more symbols;
|
changeset |
files
|
| Wed, 05 Nov 2014 22:17:05 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:59:21 +0100 |
wenzelm |
more uniform header_keywords in ML/Scala;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:21:15 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:10:38 +0100 |
wenzelm |
more frugal keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 20:49:30 +0100 |
wenzelm |
eliminated pointless dynamic keywords (TTY legacy);
|
changeset |
files
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 20:05:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 05 Nov 2014 17:37:25 +0100 |
wenzelm |
clarified representation of type Keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 16:57:12 +0100 |
wenzelm |
explicit type Keyword.Keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 15:32:11 +0100 |
wenzelm |
clarified minor/major lexicon (like ML version);
|
changeset |
files
|
| Wed, 05 Nov 2014 19:43:17 +0100 |
nipkow |
reduced execution time
|
changeset |
files
|
| Tue, 04 Nov 2014 18:19:38 +0100 |
wenzelm |
proper button margins for Nimbus L&F;
|
changeset |
files
|
| Tue, 04 Nov 2014 17:37:15 +0100 |
wenzelm |
approximative update of versions;
|
changeset |
files
|
| Tue, 04 Nov 2014 17:33:08 +0100 |
lammich |
Added Option.bind_split{,_asm,s}
|
changeset |
files
|
| Mon, 03 Nov 2014 15:08:15 +0100 |
wenzelm |
clarified legacy code;
|
changeset |
files
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
changeset |
files
|
| Mon, 03 Nov 2014 14:31:15 +0100 |
wenzelm |
eliminated obsolete Proof.goal_message -- print outcome more directly;
|
changeset |
files
|
| Mon, 03 Nov 2014 09:25:23 +0100 |
wenzelm |
updated to scala-2.11.4;
|
changeset |
files
|
| Sun, 02 Nov 2014 23:13:31 +0100 |
wenzelm |
less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:21:14 +0100 |
wenzelm |
prefer \setisabellecontext;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:16:19 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:58:35 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:39:52 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:36:52 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:27:22 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:23:48 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:16:01 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:14:15 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:13:28 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:59:40 +0100 |
wenzelm |
clarified legacy command;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:54:06 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:50:42 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:47:45 +0100 |
wenzelm |
added update_header tool;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:39:54 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:09:35 +0100 |
wenzelm |
more flexibile \setisabellecontext, independently of header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:05:43 +0100 |
wenzelm |
prefer explicit heading command;
|
changeset |
files
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
changeset |
files
|
| Sun, 02 Nov 2014 13:26:20 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Sat, 01 Nov 2014 20:19:07 +0100 |
wenzelm |
clarified syntax -- avoid overlap with command category;
|
changeset |
files
|
| Sat, 01 Nov 2014 19:47:48 +0100 |
wenzelm |
tuned signature (see ab2483fad861);
|
changeset |
files
|
| Sat, 01 Nov 2014 19:33:51 +0100 |
wenzelm |
recover via scanner;
|
changeset |
files
|
| Sat, 01 Nov 2014 18:46:48 +0100 |
wenzelm |
simplified -- scanning is never interactive;
|
changeset |
files
|
| Sat, 01 Nov 2014 15:35:40 +0100 |
wenzelm |
tuned signature, in accordance to Scala version;
|
changeset |
files
|
| Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
changeset |
files
|
| Sat, 01 Nov 2014 14:20:38 +0100 |
wenzelm |
eliminated spurious semicolons;
|
changeset |
files
|
| Sat, 01 Nov 2014 11:40:55 +0100 |
wenzelm |
eliminated former Proof General preferences;
|
changeset |
files
|
| Fri, 31 Oct 2014 23:51:54 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 31 Oct 2014 22:48:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 31 Oct 2014 22:37:22 +0100 |
wenzelm |
provide explicit theory (amending 621c052789b4);
|
changeset |
files
|
| Fri, 31 Oct 2014 22:09:18 +0100 |
wenzelm |
removed pointless markup;
|
changeset |
files
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:48:40 +0100 |
wenzelm |
discontinued obsolete control command category;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:35:11 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:20:06 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
changeset |
files
|
| Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
changeset |
files
|
| Fri, 31 Oct 2014 17:08:54 +0100 |
wenzelm |
eliminated odd flags and hook;
|
changeset |
files
|
| Fri, 31 Oct 2014 16:56:23 +0100 |
wenzelm |
avoid noise (cf. 03ff4d1e6784);
|
changeset |
files
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
changeset |
files
|
| Fri, 31 Oct 2014 15:15:10 +0100 |
wenzelm |
removed obsolete Proof General commands;
|
changeset |
files
|
| Fri, 31 Oct 2014 15:08:51 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
changeset |
files
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
changeset |
files
|
| Fri, 31 Oct 2014 17:01:54 +0000 |
paulson |
Some comments and a new version of a result
|
changeset |
files
|
| Thu, 30 Oct 2014 23:14:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:17:56 +0100 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Thu, 30 Oct 2014 15:57:13 +0100 |
wenzelm |
hardwired imitation of copy.shortcut2 default;
|
changeset |
files
|
| Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
changeset |
files
|
| Thu, 30 Oct 2014 16:36:44 +0000 |
paulson |
choose_reduce_nat: re-ordered operands
|
changeset |
files
|
| Thu, 30 Oct 2014 11:24:53 +0100 |
wenzelm |
make SML/NJ more happy;
|
changeset |
files
|
| Thu, 30 Oct 2014 11:08:26 +0100 |
wenzelm |
proper syntax categery "name" -- as usual and as documented;
|
changeset |
files
|
| Thu, 30 Oct 2014 09:15:54 +0100 |
hoelzl |
disable coercions for NO_MATCH
|
changeset |
files
|
| Wed, 29 Oct 2014 19:26:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Oct 2014 19:13:19 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 19:23:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 17:01:44 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:28:27 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:15:17 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:07:53 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:02:29 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:40:14 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:14:36 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:05:36 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 13:57:20 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 13:42:38 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:41:54 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:33:29 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:19:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:13:24 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 10:58:41 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 10:35:00 +0100 |
wenzelm |
more standard theory name;
|
changeset |
files
|
| Wed, 29 Oct 2014 09:42:46 +0100 |
wenzelm |
more iterators;
|
changeset |
files
|
| Wed, 29 Oct 2014 12:01:39 +0100 |
nipkow |
removed useless lemmas
|
changeset |
files
|
| Wed, 29 Oct 2014 11:03:23 +0100 |
nipkow |
tuned layout and proofs
|
changeset |
files
|
| Tue, 28 Oct 2014 17:16:22 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:44:58 +0100 |
wenzelm |
increase chances that HOL-Proofs image still works for polyml-5.3.0;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:27:11 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:20:26 +0100 |
wenzelm |
proper selectMatch, e.g. relevant for S-click on gutter;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:19:04 +0100 |
wenzelm |
find command span in buffer;
|
changeset |
files
|
| Tue, 28 Oct 2014 13:52:54 +0100 |
wenzelm |
'notepad' requires proper nesting of begin/end;
|
changeset |
files
|
| Tue, 28 Oct 2014 11:42:51 +0100 |
wenzelm |
explicit keyword category for commands that may start a block;
|
changeset |
files
|
| Tue, 28 Oct 2014 11:27:57 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Tue, 28 Oct 2014 10:35:38 +0100 |
wenzelm |
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:57:12 +0100 |
wenzelm |
more abstract type;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:32:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:20:07 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:31:51 +0100 |
wenzelm |
updated to jdk-7u72;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:21:56 +0100 |
wenzelm |
increase chances that HOL-Proofs image still works for polyml-5.3.0;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:20:53 +0100 |
wenzelm |
JRE is sufficient for official release -- javac and jar are only needed for self-build;
|
changeset |
files
|
| Mon, 27 Oct 2014 16:11:24 +0100 |
wenzelm |
clarified ISABELLE_JDK_HOME vs. JAVA_HOME;
|
changeset |
files
|
| Mon, 27 Oct 2014 16:00:04 +0100 |
wenzelm |
ISABELLE_JAVA_EXT is obsolete;
|
changeset |
files
|
| Mon, 27 Oct 2014 12:21:24 +0100 |
hoelzl |
further generalization of natfloor_div_nat
|
changeset |
files
|
| Mon, 27 Oct 2014 12:03:13 +0100 |
hoelzl |
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
|
changeset |
files
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
changeset |
files
|
| Sat, 25 Oct 2014 19:20:28 +0200 |
haftmann |
more simp rules;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:57:10 +0100 |
wenzelm |
clarified default;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:46:02 +0100 |
wenzelm |
support negative extraLineSpacing;
|
changeset |
files
|
| Sat, 25 Oct 2014 21:16:32 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 25 Oct 2014 11:53:35 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 24 Oct 2014 20:49:23 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:30:39 +0200 |
wenzelm |
discontinued python from standard system environment;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:05:19 +0200 |
wenzelm |
more generous default;
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:41 +0200 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:49 +0200 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
changeset |
files
|
| Thu, 23 Oct 2014 16:25:08 +0200 |
haftmann |
repaired long-standing accident
|
changeset |
files
|
| Thu, 23 Oct 2014 14:43:51 +0200 |
haftmann |
explicit definition restores HOL Light import after cb9d84d3e7f2
|
changeset |
files
|
| Thu, 23 Oct 2014 14:43:48 +0200 |
haftmann |
tuned language and spelling
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
slight generalization and unification of simp rules for algebraic procedures
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
parity induction over natural numbers
|
changeset |
files
|
| Wed, 22 Oct 2014 23:15:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 22 Oct 2014 17:34:01 +0200 |
wenzelm |
proper line height and text base line, like regular TextAreaPainter.PaintText;
|
changeset |
files
|
| Wed, 22 Oct 2014 17:30:58 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Wed, 22 Oct 2014 17:34:19 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Wed, 22 Oct 2014 13:58:30 +0200 |
Andreas Lochbihler |
add print translation for probability notation \<P>
|
changeset |
files
|
| Wed, 22 Oct 2014 17:04:45 +0200 |
wenzelm |
find main command keyword of 'begin';
|
changeset |
files
|
| Wed, 22 Oct 2014 16:44:57 +0200 |
wenzelm |
restricted scanning;
|
changeset |
files
|