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