Tue, 16 Aug 2005 19:25:32 +0200 nipkow added quite a few functions for code generation
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Tue, 16 Aug 2005 13:54:24 +0200 nipkow added listT
Tue, 16 Aug 2005 13:42:53 +0200 wenzelm support for document versions;
Tue, 16 Aug 2005 13:42:52 +0200 wenzelm eliminated datatype token;
Tue, 16 Aug 2005 13:42:51 +0200 wenzelm begin_index: list of docs;
Tue, 16 Aug 2005 13:42:50 +0200 wenzelm added eq_syntax;
Tue, 16 Aug 2005 13:42:49 +0200 wenzelm export proof_syntax, proof_of;
Tue, 16 Aug 2005 13:42:48 +0200 wenzelm added String.isSuffix;
Tue, 16 Aug 2005 13:42:47 +0200 wenzelm state: body context;
Tue, 16 Aug 2005 13:42:46 +0200 wenzelm P.tags;
Tue, 16 Aug 2005 13:42:45 +0200 wenzelm use_dir: removed hidden, added doc_versions;
Tue, 16 Aug 2005 13:42:44 +0200 wenzelm back: removed ill-defined '!' option;
Tue, 16 Aug 2005 13:42:43 +0200 wenzelm added transfer;
Tue, 16 Aug 2005 13:42:42 +0200 wenzelm moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
Tue, 16 Aug 2005 13:42:41 +0200 wenzelm added tags parser;
Tue, 16 Aug 2005 13:42:40 +0200 wenzelm clarify is_newline vs. is_blank;
Tue, 16 Aug 2005 13:42:39 +0200 wenzelm default tags for theory/proof/ML commands;
Tue, 16 Aug 2005 13:42:38 +0200 wenzelm reimplemented theory presentation, with support for tagged command regions;
Tue, 16 Aug 2005 13:42:37 +0200 wenzelm back: removed ill-defined '!' option;
Tue, 16 Aug 2005 13:42:36 +0200 wenzelm replaced sign by thy;
Tue, 16 Aug 2005 13:42:35 +0200 wenzelm added liberal_name;
Tue, 16 Aug 2005 13:42:34 +0200 wenzelm tuned Symbol.spaces;
Tue, 16 Aug 2005 13:42:33 +0200 wenzelm tuned Buffer.add;
Tue, 16 Aug 2005 13:42:32 +0200 wenzelm tuned unsuffix/unprefix;
Tue, 16 Aug 2005 13:42:31 +0200 wenzelm type proof: theory_ref instead of theory (make proof contexts independent entities);
Tue, 16 Aug 2005 13:42:30 +0200 wenzelm Isar command keyword classification (from Isar/outer_syntax.ML);
Tue, 16 Aug 2005 13:42:29 +0200 wenzelm added Isar/outer_keyword.ML;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Tue, 16 Aug 2005 13:42:23 +0200 wenzelm updated;
Tue, 16 Aug 2005 13:42:21 +0200 wenzelm removed -H false;
Tue, 16 Aug 2005 13:42:20 +0200 wenzelm isatool usedir: option -V and -f;
Tue, 16 Aug 2005 13:42:19 +0200 wenzelm tuned antiquotations;
Tue, 16 Aug 2005 13:42:18 +0200 wenzelm \isabellestyleit: proper \isacharbackslash;
Tue, 16 Aug 2005 13:42:17 +0200 wenzelm proper ML_DBASE for .../bin/poly;
Tue, 16 Aug 2005 13:42:16 +0200 wenzelm added option -V VERSION;
Tue, 16 Aug 2005 13:42:15 +0200 wenzelm added option -n NAME and -t TAGS;
Tue, 16 Aug 2005 13:42:14 +0200 wenzelm -V outline=/proof,/ML;
Tue, 16 Aug 2005 13:42:13 +0200 wenzelm * Command tags control specific markup of certain regions of text (replaces usedir -H);
Tue, 16 Aug 2005 12:51:07 +0200 nipkow simp_depth warning now mod 20, not mod 10 (too often)
Mon, 15 Aug 2005 21:39:15 +0200 dixon lucas - added pretty printing function and cleaned up signature a little.
Mon, 15 Aug 2005 21:38:25 +0200 dixon lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.
Wed, 10 Aug 2005 15:29:56 +0200 ballarin New command: interpretation in locales.
Tue, 09 Aug 2005 19:10:30 +0200 nipkow moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
Tue, 09 Aug 2005 15:44:24 +0200 haftmann exported after_qed for arity proofs
Tue, 09 Aug 2005 11:44:38 +0200 nipkow added finite(option) to Recdef.thy
Tue, 09 Aug 2005 11:00:44 +0200 haftmann added selectors 'classes_of' and 'classes_arities_of'
Tue, 09 Aug 2005 10:23:14 +0200 haftmann exported dest_def
Tue, 09 Aug 2005 10:03:30 +0200 haftmann added 'the_const_constraint'
Tue, 09 Aug 2005 08:56:34 +0200 haftmann (added to repository)
Tue, 09 Aug 2005 08:54:41 +0200 haftmann (added to repository)
Mon, 08 Aug 2005 22:14:04 +0200 ballarin After_qed takes result argument.
Mon, 08 Aug 2005 22:11:31 +0200 ballarin Release of interpretation in locale.
Mon, 08 Aug 2005 12:15:03 +0200 nipkow fixed typo in ratadd
Mon, 08 Aug 2005 09:29:16 +0200 haftmann added hint for position of aqu options in connection with styles
Mon, 08 Aug 2005 09:28:25 +0200 haftmann clarified ML_idf
Sun, 07 Aug 2005 12:30:45 +0200 nipkow moved some rat functions to library.ML
Sun, 07 Aug 2005 12:28:10 +0200 nipkow added more rat functions
Sat, 06 Aug 2005 18:06:56 +0200 berghofe Tuned comment.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip