NEWS
Wed, 08 Apr 2015 19:15:55 +0200 blanchet Z3 news
Wed, 08 Apr 2015 15:21:20 +0200 blanchet renamed multiset ordering to free up nice <# etc. symbols for the standard subset
Wed, 08 Apr 2015 11:13:53 +0200 wenzelm misc tuning for release;
Tue, 07 Apr 2015 18:21:56 +0200 nipkow Removed mcard because it is equal to size
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Sat, 04 Apr 2015 22:01:30 +0200 wenzelm some explanation of 'private';
Wed, 01 Apr 2015 22:40:41 +0200 wenzelm merged
Wed, 01 Apr 2015 22:08:06 +0200 wenzelm added command 'experiment';
Wed, 01 Apr 2015 19:31:28 +0200 wenzelm NEWS;
Wed, 01 Apr 2015 16:24:38 +0200 wenzelm added isabelle build option -x, to exclude sessions;
Wed, 01 Apr 2015 15:41:08 +0200 wenzelm added isabelle build option -k, for fast off-line checking of theory sources;
Wed, 01 Apr 2015 14:48:38 +0100 paulson HOL Light Libraries for complex Arctan, Arcsin, Arccos
Tue, 31 Mar 2015 21:54:32 +0200 haftmann NEWS
Mon, 30 Mar 2015 00:13:37 +0200 wenzelm clarified NEWS (cf. 97872c658a44);
Sun, 29 Mar 2015 16:22:35 +0200 wenzelm rule_insts_schematic is considered legacy and false by default;
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
less more (0) -1000 -300 -100 -60 tip