src/Pure/Isar/method.ML
Thu, 02 Apr 2015 20:28:30 +0200 wenzelm proper treatment of internal method name as already checked Token.src;
Thu, 02 Apr 2015 14:11:00 +0200 wenzelm clarified method_closure;
Thu, 02 Apr 2015 11:41:14 +0200 wenzelm tuned signature;
Tue, 10 Mar 2015 13:55:10 +0100 wenzelm clarified Token.check_src: intern at most once;
Mon, 09 Mar 2015 20:33:33 +0100 wenzelm support structural composition (THEN_ALL_NEW) for proof methods;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sun, 30 Nov 2014 14:02:48 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Wed, 12 Nov 2014 10:30:59 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Tue, 11 Nov 2014 20:11:38 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
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.;
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Thu, 28 Aug 2014 13:25:12 +0200 wenzelm intern xthm only once;
Wed, 27 Aug 2014 14:54:32 +0200 wenzelm more explicit Method.modifier with reported position;
Fri, 22 Aug 2014 15:55:24 +0200 wenzelm attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
Fri, 22 Aug 2014 11:28:51 +0200 wenzelm made SML/NJ happy;
Thu, 21 Aug 2014 23:54:27 +0200 wenzelm clarified Method.section: explicit declaration with static closure;
Thu, 21 Aug 2014 13:31:31 +0200 wenzelm tuned;
Thu, 21 Aug 2014 09:48:59 +0200 wenzelm tuned;
Wed, 20 Aug 2014 17:30:43 +0200 wenzelm proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
Wed, 20 Aug 2014 16:06:10 +0200 wenzelm more uniform data slot;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Tue, 19 Aug 2014 16:46:07 +0200 wenzelm just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
Tue, 19 Aug 2014 16:09:11 +0200 wenzelm tuned signature;
Tue, 19 Aug 2014 15:55:06 +0200 wenzelm more compact datatypes;
Tue, 19 Aug 2014 15:10:37 +0200 wenzelm tuned;
Tue, 19 Aug 2014 14:51:25 +0200 wenzelm clarifed Method.evaluate: turn text into semantic method (like Basic);
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Thu, 14 Aug 2014 14:28:11 +0200 wenzelm localized command 'method_setup' and 'attribute_setup';
Thu, 14 Aug 2014 12:33:21 +0200 wenzelm tuned;
Thu, 14 Aug 2014 12:13:24 +0200 wenzelm tuned;
Thu, 14 Aug 2014 11:51:17 +0200 wenzelm localized method definitions (see also f14c1248d064);
Tue, 05 Aug 2014 15:07:11 +0200 wenzelm avoid duplication of warnings stemming from simp/intro declarations etc.;
Wed, 09 Apr 2014 20:58:32 +0200 wenzelm proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Thu, 20 Mar 2014 22:00:13 +0100 wenzelm more static checking of proof methods;
Tue, 18 Mar 2014 15:29:58 +0100 wenzelm more antiquotations;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only;
Mon, 10 Mar 2014 15:04:01 +0100 wenzelm tuned signature -- prefer Name_Space.get with its builtin error;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
Wed, 05 Mar 2014 15:25:52 +0100 wenzelm special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Fri, 28 Feb 2014 10:40:04 +0100 wenzelm more explicit method reports;
Wed, 26 Feb 2014 11:58:35 +0100 wenzelm markup for method combinators;
Wed, 26 Feb 2014 10:40:13 +0100 wenzelm method language markup, e.g. relevant to prevent outer keyword completion;
Tue, 25 Feb 2014 14:34:18 +0100 wenzelm modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
Mon, 24 Feb 2014 10:48:34 +0100 wenzelm clarified Token.range_of in accordance to Symbol_Pos.range;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Sun, 19 Jan 2014 21:33:45 +0100 wenzelm implicit "cartouche" method (experimental, undocumented);
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
less more (0) -300 -100 -60 tip