Sat, 09 Aug 2008 22:43:58 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 09 Aug 2008 22:43:57 +0200 wenzelm unified Args.T with OuterLex.token;
Sat, 09 Aug 2008 22:43:56 +0200 wenzelm unified Args.T with OuterLex.token;
Sat, 09 Aug 2008 22:43:55 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 09 Aug 2008 22:43:54 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 09 Aug 2008 22:43:53 +0200 wenzelm unified Args.T with OuterLex.token;
Sat, 09 Aug 2008 22:43:52 +0200 wenzelm load args.ML later (after outer_parse.ML);
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 09 Aug 2008 12:28:13 +0200 wenzelm read_asts: report literal tokens;
Sat, 09 Aug 2008 12:28:12 +0200 wenzelm tuned error message;
Sat, 09 Aug 2008 12:28:11 +0200 wenzelm pos_of_token: Position.T;
Sat, 09 Aug 2008 12:28:10 +0200 wenzelm dest: sort strings;
Sat, 09 Aug 2008 12:28:09 +0200 wenzelm added literal;
Sat, 09 Aug 2008 00:09:39 +0200 wenzelm read_token: more robust handling of empty text;
Sat, 09 Aug 2008 00:09:38 +0200 wenzelm datatype token: maintain range, tuned representation;
Sat, 09 Aug 2008 00:09:36 +0200 wenzelm datatype token: maintain range, tuned representation;
Sat, 09 Aug 2008 00:09:35 +0200 wenzelm datatype token: maintain range, tuned representation;
Sat, 09 Aug 2008 00:09:34 +0200 wenzelm tuned SymbolPos interface;
Sat, 09 Aug 2008 00:09:31 +0200 wenzelm YXML.parse: allow text without markup, potentially empty;
Sat, 09 Aug 2008 00:09:29 +0200 wenzelm added content;
Sat, 09 Aug 2008 00:09:26 +0200 wenzelm added distance_of (permissive version);
Fri, 08 Aug 2008 19:29:01 +0200 wenzelm count offset as well;
Fri, 08 Aug 2008 19:28:59 +0200 wenzelm added offset/end_offset;
Fri, 08 Aug 2008 16:54:33 +0200 wenzelm tuned formatting;
Fri, 08 Aug 2008 15:36:40 +0200 krauss clean up dead code
Fri, 08 Aug 2008 13:36:44 +0200 wenzelm made SML/NJ happy;
Fri, 08 Aug 2008 09:44:16 +0200 krauss FundefLib.try_proof : attempt a proof and see if it works
Fri, 08 Aug 2008 09:26:15 +0200 nipkow added lemmas
Thu, 07 Aug 2008 23:56:45 +0200 wenzelm inner_syntax markup is back;
Thu, 07 Aug 2008 23:32:49 +0200 wenzelm disabled inner_syntax markup for now;
Thu, 07 Aug 2008 22:32:03 +0200 wenzelm added read_token -- with optional YXML encoding of position;
Thu, 07 Aug 2008 22:32:01 +0200 wenzelm parse_token: use Syntax.read_token, pass full position information;
Thu, 07 Aug 2008 21:13:01 +0200 wenzelm tuned;
Thu, 07 Aug 2008 21:07:57 +0200 wenzelm map_default: more explicit scope;
Thu, 07 Aug 2008 21:07:55 +0200 wenzelm datatype lexicon: alternative representation using nested Symtab.table;
Thu, 07 Aug 2008 19:21:43 +0200 wenzelm simplified Antiquote signature;
Thu, 07 Aug 2008 19:21:42 +0200 wenzelm more precise positions due to SymbolsPos.implode_delim;
Thu, 07 Aug 2008 19:21:41 +0200 wenzelm simplified Antiq: regular SymbolPos.text with position;
Thu, 07 Aug 2008 19:21:40 +0200 wenzelm renamed SymbolPos.scan_position to SymbolPos.scan_pos;
Thu, 07 Aug 2008 19:21:39 +0200 wenzelm only increment column if valid;
Thu, 07 Aug 2008 19:21:38 +0200 wenzelm install_pp Position.T;
Thu, 07 Aug 2008 19:21:37 +0200 wenzelm Position.start;
Thu, 07 Aug 2008 13:45:15 +0200 wenzelm SymbolPos.explode;
Thu, 07 Aug 2008 13:45:13 +0200 wenzelm improved position handling due to SymbolPos.T;
Thu, 07 Aug 2008 13:45:11 +0200 wenzelm improved position handling due to SymbolPos.T;
Thu, 07 Aug 2008 13:45:09 +0200 wenzelm Antiquote.read/read_arguments;
Thu, 07 Aug 2008 13:45:07 +0200 wenzelm updated type of nested sources;
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);
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip