Thu, 07 Aug 2008 13:45:05 +0200 wenzelm improved position handling due to SymbolPos.T;
Thu, 07 Aug 2008 13:45:03 +0200 wenzelm adapted Scan.extend_lexicon/merge_lexicons;
Thu, 07 Aug 2008 13:44:56 +0200 wenzelm renamed scan_antiquotes to read;
Thu, 07 Aug 2008 13:44:52 +0200 wenzelm export not_eof;
Thu, 07 Aug 2008 13:44:47 +0200 wenzelm reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
Thu, 07 Aug 2008 13:44:42 +0200 wenzelm advance: single argument (again);
Thu, 07 Aug 2008 13:44:36 +0200 wenzelm Symbols with explicit position information.
Thu, 07 Aug 2008 13:44:33 +0200 wenzelm added General/symbol_pos.ML;
Wed, 06 Aug 2008 16:41:40 +0200 ballarin Interpretation command (theory/proof context) no longer simplifies goal.
Wed, 06 Aug 2008 13:57:25 +0200 nipkow added lemma
Wed, 06 Aug 2008 10:43:42 +0200 wenzelm made SML/NJ happy;
Wed, 06 Aug 2008 00:58:27 +0200 berghofe Reverted last change, since it caused incompatibilities.
Wed, 06 Aug 2008 00:12:31 +0200 wenzelm fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
Wed, 06 Aug 2008 00:12:26 +0200 wenzelm T.end_position_of;
Wed, 06 Aug 2008 00:12:21 +0200 wenzelm adapted Antiq;
Wed, 06 Aug 2008 00:12:02 +0200 wenzelm parse_sort/typ/term/prop: report markup;
Wed, 06 Aug 2008 00:11:12 +0200 wenzelm sort/typ/term/prop: inner_syntax markup encodes original source position;
Wed, 06 Aug 2008 00:10:31 +0200 wenzelm removed obsolete range_of (already included in position);
Wed, 06 Aug 2008 00:10:22 +0200 wenzelm report markup;
Wed, 06 Aug 2008 00:10:18 +0200 wenzelm Antiq: inner vs. outer position;
Wed, 06 Aug 2008 00:10:13 +0200 wenzelm of_properties: observe Markup.position_properties';
Wed, 06 Aug 2008 00:10:08 +0200 wenzelm added position_properties';
Tue, 05 Aug 2008 19:29:09 +0200 wenzelm token: maintain of source, which retains original position information;
Tue, 05 Aug 2008 19:29:08 +0200 wenzelm moved OuterLex.count here;
Tue, 05 Aug 2008 19:29:07 +0200 wenzelm improved recover: also resync on symbol/comment/verbatim delimiters;
Tue, 05 Aug 2008 19:29:06 +0200 wenzelm advance: operate on symbol list (less overhead);
Tue, 05 Aug 2008 19:29:02 +0200 wenzelm added token;
Tue, 05 Aug 2008 14:40:48 +0200 krauss fix HOL/ex/LexOrds.thy; add to regression
Tue, 05 Aug 2008 13:31:38 +0200 wenzelm added report;
Tue, 05 Aug 2008 13:31:36 +0200 wenzelm removed axiom;
Tue, 05 Aug 2008 13:31:35 +0200 wenzelm get_fact: report position;
Tue, 05 Aug 2008 13:31:31 +0200 wenzelm Facts.lookup: return static/dynamic status;
Mon, 04 Aug 2008 22:55:10 +0200 wenzelm position scanner: encode token range;
Mon, 04 Aug 2008 22:55:08 +0200 wenzelm added encode_range;
Mon, 04 Aug 2008 22:55:04 +0200 wenzelm added end_line, end_column properties;
Mon, 04 Aug 2008 22:55:00 +0200 wenzelm meta_subst: xsymbols make it work with clean Pure;
Mon, 04 Aug 2008 21:24:19 +0200 wenzelm abstract type Scan.stopper, position taken from last input token;
Mon, 04 Aug 2008 21:24:17 +0200 wenzelm abstract type Scan.stopper;
Mon, 04 Aug 2008 21:24:15 +0200 wenzelm abstract type stopper, may depend on final input;
Mon, 04 Aug 2008 20:27:40 +0200 wenzelm removed obsolete apply_theorems(_i);
Mon, 04 Aug 2008 20:27:39 +0200 wenzelm tuned signature;
Mon, 04 Aug 2008 20:27:38 +0200 wenzelm removed obsolete note_thms_cmd;
Mon, 04 Aug 2008 20:27:37 +0200 wenzelm simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
Mon, 04 Aug 2008 20:19:59 +0200 wenzelm tuned description;
Mon, 04 Aug 2008 19:25:59 +0200 wenzelm replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
Mon, 04 Aug 2008 18:57:35 +0200 berghofe Quoted terms in consts_code declarations are now preprocessed as well.
Mon, 04 Aug 2008 18:56:55 +0200 berghofe Exported eval_wrapper.
Mon, 04 Aug 2008 18:56:22 +0200 berghofe - corrected bogus comment for function inst_conj_all
Mon, 04 Aug 2008 18:24:27 +0200 krauss removed dead code
Mon, 04 Aug 2008 17:13:34 +0200 wenzelm simplified prepare_command;
Mon, 04 Aug 2008 17:13:33 +0200 wenzelm Isar.command: explicitly set transaction position, as required for prepare_command errors;
Mon, 04 Aug 2008 10:37:33 +0200 ballarin Updated locale tests.
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Fri, 01 Aug 2008 17:41:37 +0200 ballarin Removed import and lparams from locale record.
Fri, 01 Aug 2008 12:57:50 +0200 nipkow made setsum executable on int.
Thu, 31 Jul 2008 09:49:21 +0200 ballarin Tuned (for the sake of a meaningless log entry).
Wed, 30 Jul 2008 19:03:33 +0200 ballarin New locales for orders and lattices where the equivalence relation is not restricted to equality.
Wed, 30 Jul 2008 16:07:00 +0200 nipkow added hint about writing "x : set xs".
Wed, 30 Jul 2008 07:34:01 +0200 haftmann simple lifters
Wed, 30 Jul 2008 07:34:00 +0200 haftmann dropped imperative monad bind
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip