Thu, 18 Aug 2005 11:17:35 +0200 wenzelm updated;
Thu, 18 Aug 2005 11:17:34 +0200 wenzelm usedir: tuned option -V;
Thu, 18 Aug 2005 11:17:33 +0200 wenzelm usedir: removed option -H;
Thu, 18 Aug 2005 11:17:32 +0200 wenzelm * Proper output of proof terms within a proof context;
Wed, 17 Aug 2005 17:04:15 +0200 ballarin Improved generation of witnesses in interpretation.
Wed, 17 Aug 2005 17:03:20 +0200 ballarin Interpretation in locales.
Wed, 17 Aug 2005 17:02:16 +0200 ballarin Use interpretation in locales.
Wed, 17 Aug 2005 15:10:00 +0200 paulson new examples
Wed, 17 Aug 2005 14:19:17 +0200 nipkow *** empty log message ***
Wed, 17 Aug 2005 13:52:53 +0200 paulson new command to invoke ATPs
Wed, 17 Aug 2005 11:44:02 +0200 nipkow small mods to code lemmas
Wed, 17 Aug 2005 11:15:23 +0200 wenzelm made SML/XL happy;
Wed, 17 Aug 2005 08:06:12 +0200 nipkow list_all_conv -> iff
Tue, 16 Aug 2005 19:25:42 +0200 nipkow name fix
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
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip