| Wed, 01 Apr 2015 15:41:08 +0200 |
wenzelm |
added isabelle build option -k, for fast off-line checking of theory sources;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 14:48:38 +0100 |
paulson |
HOL Light Libraries for complex Arctan, Arcsin, Arccos
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 00:13:37 +0200 |
wenzelm |
clarified NEWS (cf. 97872c658a44);
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 16:22:35 +0200 |
wenzelm |
rule_insts_schematic is considered legacy and false by default;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 17:51:34 +0100 |
blanchet |
more multiset theorems
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:59:28 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 15:57:51 +0100 |
wenzelm |
admit dummy patterns in instantiations;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 23:16:40 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 17:23:22 +0000 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 13:51:33 +0100 |
noschinl |
added proof method rewrite
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 23:04:40 +0100 |
blanchet |
documented renamed theories
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 21:30:42 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 20:33:33 +0100 |
wenzelm |
support structural composition (THEN_ALL_NEW) for proof methods;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 16:42:18 +0000 |
paulson |
Removed the infix operator "choose" to allow HOLCF to build
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 22:38:11 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:13 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:04 +0100 |
nipkow |
Removed the obsolete functions "natfloor" and "natceiling"
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2015 08:50:00 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Fri, 27 Feb 2015 15:41:28 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:50:30 +0100 |
wenzelm |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:48 +0100 |
haftmann |
eliminated fact duplicates
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:15 +0100 |
haftmann |
dropped redundancy
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:53:56 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 13:01:12 +0100 |
haftmann |
dropped obsolete external entrance point
|
file |
diff |
annotate
|
| Mon, 26 Jan 2015 14:34:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 25 Jan 2015 22:11:06 +0100 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 20:01:48 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Tue, 06 Jan 2015 22:48:34 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 11:12:15 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 11:08:47 +0100 |
boehmes |
updated NEWS
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 11:50:34 +0100 |
wenzelm |
added system property isabelle.laf, notably for initial system dialog;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 10:38:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 20:40:37 +0100 |
wenzelm |
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 16:44:24 +0100 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
| Fri, 12 Dec 2014 14:31:57 +0100 |
wenzelm |
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 12:30:47 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 16:55:43 +0100 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:44 +0100 |
immler |
NEWS
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 16:47:45 +0100 |
wenzelm |
added update_header tool;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|