NEWS
Tue, 13 Aug 2013 17:26:22 +0200 wenzelm disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
Fri, 09 Aug 2013 20:31:51 +0200 wenzelm NEWS;
Wed, 07 Aug 2013 15:35:33 +0200 wenzelm more NEWS and CONTRIBUTORS;
Wed, 31 Jul 2013 21:53:33 +0200 wenzelm NEWS;
Wed, 31 Jul 2013 10:54:37 +0200 wenzelm simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Mon, 29 Jul 2013 20:46:21 +0200 wenzelm NEWS;
Sat, 27 Jul 2013 22:20:25 +0200 wenzelm discontinued historic document formats;
Sat, 27 Jul 2013 22:16:04 +0200 wenzelm avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
Sat, 27 Jul 2013 21:43:12 +0200 wenzelm discontinued ISABELLE_DOC_FORMAT;
Sat, 13 Jul 2013 21:02:41 +0200 wenzelm merged
Sat, 13 Jul 2013 14:13:34 +0200 wenzelm NEWS;
Sat, 13 Jul 2013 17:53:58 +0200 haftmann attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
Sun, 07 Jul 2013 18:43:14 +0200 wenzelm discontinued obsolete "isabelle print";
Sun, 07 Jul 2013 18:34:29 +0200 wenzelm discontinued command 'print_drafts';
Sat, 06 Jul 2013 21:19:38 +0200 wenzelm minimal jedit mode for Isabelle NEWS;
Sun, 30 Jun 2013 12:30:02 +0200 wenzelm discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
Sun, 30 Jun 2013 11:37:34 +0200 wenzelm backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
Thu, 27 Jun 2013 23:17:26 +0200 wenzelm manage option "proofs" within theory context -- with minor overhead for primitive inferences;
Thu, 27 Jun 2013 10:35:37 +0200 wenzelm updated documentation;
Tue, 25 Jun 2013 16:55:10 +0200 wenzelm dockable window for Isabelle documentation;
Mon, 24 Jun 2013 23:33:14 +0200 wenzelm improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 23 Jun 2013 21:23:36 +0200 wenzelm proper diagnostic command 'print_state';
Tue, 18 Jun 2013 15:31:52 +0200 wenzelm eliminated old "ref" manual;
Sat, 15 Jun 2013 17:19:23 +0200 haftmann lifting for primitive definitions;
Sun, 02 Jun 2013 07:46:40 +0200 haftmann make reification part of HOL
Fri, 31 May 2013 07:30:23 +0200 bulwahn NEWS about Spec_Check
Sat, 25 May 2013 18:30:38 +0200 wenzelm merged
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
Wed, 22 May 2013 18:10:54 +0200 wenzelm added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
Fri, 17 May 2013 20:53:28 +0200 wenzelm renamed 'print_configs' to 'print_options';
Fri, 17 May 2013 20:41:45 +0200 wenzelm proper option quick_and_dirty;
Fri, 17 May 2013 18:39:49 +0200 wenzelm discontinued obsolete isabelle-process options -f and -u;
Fri, 17 May 2013 18:23:39 +0200 wenzelm NEWS;
Fri, 17 May 2013 18:19:42 +0200 wenzelm discontinued obsolete isabelle usedir, mkdir, make;
Thu, 25 Apr 2013 11:59:21 +0200 hoelzl revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
Thu, 25 Apr 2013 10:35:56 +0200 hoelzl renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
Wed, 24 Apr 2013 13:28:30 +0200 hoelzl spell conditional_ly_-complete lattices correct
Tue, 23 Apr 2013 19:31:24 +0200 haftmann documentation and NEWS
Mon, 22 Apr 2013 16:36:02 +0200 hoelzl NEWS
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
Wed, 10 Apr 2013 19:14:47 +0200 wenzelm merged
Wed, 10 Apr 2013 17:02:47 +0200 wenzelm added ML antiquotation @{theory_context};
Wed, 10 Apr 2013 17:49:16 +0200 traytel NEWS and CONTRIBUTORS
Tue, 02 Apr 2013 16:29:40 +0200 wenzelm NEWS for 635562bc14ef;
Wed, 27 Mar 2013 22:36:03 +0100 ballarin Improvements to the print_dependencies command.
Wed, 27 Mar 2013 16:38:25 +0100 wenzelm more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
Tue, 26 Mar 2013 11:26:13 +0100 wenzelm dockable window for timing information;
Mon, 25 Mar 2013 20:00:27 +0100 ballarin Discontinued theories src/HOL/Algebra/abstract and .../poly.
Sat, 23 Mar 2013 20:57:57 +0100 haftmann spelling
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Sat, 23 Mar 2013 17:11:06 +0100 haftmann locales for abstract orders
Wed, 13 Mar 2013 15:12:14 +0100 wenzelm sessions may be organized via 'chapter' in ROOT;
Tue, 12 Mar 2013 16:47:24 +0100 wenzelm discontinued "isabelle usedir" option -r (reset session path);
Mon, 11 Mar 2013 14:25:14 +0100 wenzelm discontinued "isabelle usedir" option -P (remote path);
Sat, 09 Mar 2013 11:56:01 +0100 haftmann discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
less more (0) -1000 -300 -100 -60 tip