Wed, 11 Jul 2007 11:02:07 +0200 berghofe Added ML bindings for sup_fun_eq and sup_bool_eq.
Wed, 11 Jul 2007 11:01:24 +0200 berghofe top and bot are now constants.
Wed, 11 Jul 2007 11:00:46 +0200 berghofe Renamed inductive2 to inductive.
Wed, 11 Jul 2007 11:00:09 +0200 berghofe acc is now defined using inductive_set.
Wed, 11 Jul 2007 10:59:23 +0200 berghofe Added new package for inductive sets.
Wed, 11 Jul 2007 10:53:39 +0200 berghofe Adapted to new inductive definition package.
Wed, 11 Jul 2007 10:52:20 +0200 berghofe Adapted to changes in inductive definition package.
Wed, 11 Jul 2007 00:46:48 +0200 wenzelm tuned comment markup;
Wed, 11 Jul 2007 00:29:52 +0200 wenzelm treat OuterLex.Error;
Wed, 11 Jul 2007 00:29:51 +0200 wenzelm separated Malformed (symbolic char) from Error (bad input);
Wed, 11 Jul 2007 00:29:50 +0200 wenzelm Output.escape_malformed;
Wed, 11 Jul 2007 00:29:49 +0200 wenzelm added escape_malformed (failsafe);
Tue, 10 Jul 2007 23:29:53 +0200 wenzelm Basic editing of theory sources.
Tue, 10 Jul 2007 23:29:52 +0200 wenzelm tuned;
Tue, 10 Jul 2007 23:29:51 +0200 wenzelm export html_mode, begin_document, end_document;
Tue, 10 Jul 2007 23:29:49 +0200 wenzelm renamed XML.Rawtext to XML.Output;
Tue, 10 Jul 2007 23:29:47 +0200 wenzelm export get_lexicons;
Tue, 10 Jul 2007 23:29:46 +0200 wenzelm added kind_of;
Tue, 10 Jul 2007 23:29:44 +0200 wenzelm Markup.enclose;
Tue, 10 Jul 2007 23:29:43 +0200 wenzelm more markup for inner and outer syntax;
Tue, 10 Jul 2007 23:29:41 +0200 wenzelm simplified funpow, untabify;
Tue, 10 Jul 2007 23:29:38 +0200 wenzelm added Thy/thy_edit.ML;
Tue, 10 Jul 2007 23:29:35 +0200 wenzelm added some markup for outer syntax;
Tue, 10 Jul 2007 17:30:57 +0200 haftmann clarified merge of module names
Tue, 10 Jul 2007 17:30:56 +0200 haftmann now a monolithic module
Tue, 10 Jul 2007 17:30:54 +0200 haftmann now works with SML/NJ
Tue, 10 Jul 2007 17:30:53 +0200 haftmann tuned
Tue, 10 Jul 2007 17:30:52 +0200 haftmann improvement for code names
Tue, 10 Jul 2007 17:30:51 +0200 haftmann removed proof dependency on transitivity theorems
Tue, 10 Jul 2007 17:30:50 +0200 haftmann moved lfp_induct2 here
Tue, 10 Jul 2007 17:30:49 +0200 haftmann clarified import
Tue, 10 Jul 2007 17:30:47 +0200 haftmann moved lfp_induct2 to Relation.thy
Tue, 10 Jul 2007 17:30:45 +0200 haftmann moved some finite lemmas here
Tue, 10 Jul 2007 17:30:43 +0200 haftmann moved finite lemmas to Finite_Set.thy
Tue, 10 Jul 2007 16:46:37 +0200 wenzelm added print_mode setup (from pretty.ML);
Tue, 10 Jul 2007 16:45:06 +0200 wenzelm Markup.add_mode;
Tue, 10 Jul 2007 16:45:05 +0200 wenzelm removed no_state markup -- produce empty state;
Tue, 10 Jul 2007 16:45:04 +0200 wenzelm Markup.output;
Tue, 10 Jul 2007 16:45:03 +0200 wenzelm moved source cascading from scan.ML to source.ML;
Tue, 10 Jul 2007 16:45:01 +0200 wenzelm infixr || (more efficient);
Tue, 10 Jul 2007 16:45:00 +0200 wenzelm moved print_mode setup for markup to markup.ML;
Tue, 10 Jul 2007 16:45:00 +0200 wenzelm Markup.output;
Tue, 10 Jul 2007 16:44:58 +0200 wenzelm use position.ML earlier;
Tue, 10 Jul 2007 15:45:34 +0200 aspinall Add widthN to signature
Tue, 10 Jul 2007 13:12:53 +0200 wenzelm cd ISABELLE_HOME/etc;
Tue, 10 Jul 2007 09:24:43 +0200 haftmann adjusted
Tue, 10 Jul 2007 09:24:14 +0200 haftmann updated keywords
Tue, 10 Jul 2007 09:23:17 +0200 haftmann simplified, tuned
Tue, 10 Jul 2007 09:23:16 +0200 haftmann re-expanded paths
Tue, 10 Jul 2007 09:23:15 +0200 haftmann replaced code generator framework for reflected cooper
Tue, 10 Jul 2007 09:23:14 +0200 haftmann expanded fragile proof
Tue, 10 Jul 2007 09:23:13 +0200 haftmann extended - convers now basic lcm properties also
Tue, 10 Jul 2007 09:23:12 +0200 haftmann constant dvd now in class target
Tue, 10 Jul 2007 09:23:11 +0200 haftmann moved lemma zdvd_period here
Tue, 10 Jul 2007 09:23:10 +0200 haftmann introduced (auxiliary) class dvd_mod for more convenient code generation
Tue, 10 Jul 2007 00:43:51 +0200 wenzelm tuned;
Tue, 10 Jul 2007 00:17:52 +0200 wenzelm nested source: explicit interactive flag for recover avoids duplicate errors;
Mon, 09 Jul 2007 23:12:51 +0200 wenzelm tuned dead code;
Mon, 09 Jul 2007 23:12:49 +0200 wenzelm use Position.file_of;
Mon, 09 Jul 2007 23:12:46 +0200 wenzelm toplevel_source: interactive flag indicates intermittent error_msg;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip