src/Pure/Pure.thy
Sun, 26 Jan 2014 14:01:19 +0100 wenzelm discontinued obsolete attribute "standard";
Sat, 25 Jan 2014 18:34:05 +0100 wenzelm prefer self-contained user-space tool;
Sat, 25 Jan 2014 18:18:03 +0100 wenzelm define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
Fri, 17 Jan 2014 20:31:39 +0100 wenzelm prefer user-space tool within Pure.thy;
Thu, 12 Dec 2013 21:28:13 +0100 wenzelm skeleton for Simplifier trace by Lars Hupel;
Wed, 18 Sep 2013 11:08:28 +0200 wenzelm moved module into plain Isabelle/ML user space;
Wed, 11 Sep 2013 20:16:28 +0200 wenzelm more explicit indication of 'done' as proof script element;
Mon, 02 Sep 2013 16:10:26 +0200 wenzelm more explicit indication of 'guess' as improper Isar (aka "script") element;
Sun, 07 Jul 2013 18:34:29 +0200 wenzelm discontinued command 'print_drafts';
Tue, 25 Jun 2013 20:35:50 +0200 wenzelm recover command tags from 4cf3f6153eb8 -- important for document preparation;
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;
Mon, 24 Jun 2013 17:17:17 +0200 wenzelm back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
Mon, 24 Jun 2013 17:03:53 +0200 wenzelm more formal ProofGeneral command setup within theory Pure;
Sun, 23 Jun 2013 21:23:36 +0200 wenzelm proper diagnostic command 'print_state';
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 17 May 2013 20:53:28 +0200 wenzelm renamed 'print_configs' to 'print_options';
Wed, 15 May 2013 20:34:42 +0200 wenzelm moved files;
Wed, 15 May 2013 20:22:46 +0200 wenzelm maintain ProofGeneral preferences within ProofGeneral module;
Sat, 30 Mar 2013 14:57:06 +0100 wenzelm added 'print_defn_rules' command;
Thu, 28 Feb 2013 16:38:17 +0100 wenzelm discontinued obsolete 'axioms' command;
Wed, 27 Feb 2013 17:32:17 +0100 wenzelm discontinued redundant 'use' command;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Mon, 25 Feb 2013 13:29:19 +0100 wenzelm discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
Mon, 25 Feb 2013 11:07:02 +0100 wenzelm reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
Tue, 19 Feb 2013 21:44:37 +0100 wenzelm back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
Wed, 19 Dec 2012 22:26:26 +0100 nipkow removed odd associativity of ==
Mon, 19 Nov 2012 22:34:17 +0100 wenzelm alternative completion for outer syntax keywords;
Wed, 26 Sep 2012 14:23:33 +0200 wenzelm tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
Sun, 26 Aug 2012 22:23:10 +0200 wenzelm entity markup for theory Pure, to enable hyperlinks etc.;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 02 Aug 2012 12:36:54 +0200 wenzelm more official command specifications, including source position;
Wed, 01 Aug 2012 23:33:26 +0200 wenzelm more standard bootstrapping of Pure outer syntax;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 20 Nov 2008 00:03:47 +0100 wenzelm Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
Tue, 28 Oct 2008 11:03:07 +0100 ballarin Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
Fri, 25 Jul 2008 12:03:32 +0200 haftmann dropped locale (open)
Sun, 18 May 2008 17:03:23 +0200 wenzelm converted to regular application syntax;
Mon, 07 Apr 2008 21:29:46 +0200 wenzelm prefer plain ASCII here;
Mon, 07 Apr 2008 21:25:21 +0200 wenzelm added swap_params;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 27 Mar 2008 14:41:12 +0100 wenzelm reduced to theory body (cf. OuterSyntax.process_file);
Tue, 17 Jul 2007 13:19:19 +0200 wenzelm moved print_translations from Pure.thy to Syntax/syn_trans.ML;
Wed, 20 Jun 2007 08:09:56 +0200 nipkow added meta_impE
Fri, 11 May 2007 01:07:10 +0200 wenzelm tuned proofs;
Sat, 02 Dec 2006 14:59:25 +0100 wenzelm meta_term_syntax: proper operation on untyped preterms;
Sat, 02 Dec 2006 02:52:07 +0100 wenzelm added some support for embedded terms;
Tue, 19 Sep 2006 23:15:36 +0200 wenzelm revert to previous version;
Tue, 19 Sep 2006 15:22:03 +0200 haftmann (void)
Tue, 06 Jun 2006 20:47:12 +0200 wenzelm removed Toplevel.debug;
Tue, 06 Jun 2006 10:05:57 +0200 ballarin Improved parameter management of locales.
Wed, 22 Feb 2006 22:18:32 +0100 wenzelm simplified Pure conjunction;
Wed, 15 Feb 2006 21:34:59 +0100 wenzelm cannot use section before setup;
Sun, 29 Jan 2006 19:23:43 +0100 wenzelm tuned proofs;
Thu, 19 Jan 2006 21:22:15 +0100 wenzelm tuned comments;
Fri, 13 Jan 2006 01:12:59 +0100 wenzelm implicit setup, which admits exception_trace;
Thu, 22 Dec 2005 00:28:52 +0100 wenzelm added locale meta_conjunction_syntax and various conjunction rules;
Fri, 28 Oct 2005 22:26:10 +0200 wenzelm tuned;
Sat, 23 Apr 2005 19:49:39 +0200 wenzelm tuned proofs;
Thu, 21 Apr 2005 22:06:00 +0200 wenzelm The Pure theory.
less more (0) tip