2007-07-10 haftmann 2007-07-10 moved lfp_induct2 here
2007-07-10 haftmann 2007-07-10 clarified import
2007-07-10 haftmann 2007-07-10 moved lfp_induct2 to Relation.thy
2007-07-10 haftmann 2007-07-10 moved some finite lemmas here
2007-07-10 haftmann 2007-07-10 moved finite lemmas to Finite_Set.thy
2007-07-10 wenzelm 2007-07-10 added print_mode setup (from pretty.ML); removed no_state;
2007-07-10 wenzelm 2007-07-10 Markup.add_mode;
2007-07-10 wenzelm 2007-07-10 removed no_state markup -- produce empty state; Markup.add_mode;
2007-07-10 wenzelm 2007-07-10 Markup.output; removed no_state markup -- produce empty state;
2007-07-10 wenzelm 2007-07-10 moved source cascading from scan.ML to source.ML;
2007-07-10 wenzelm 2007-07-10 infixr || (more efficient); tuned signature; removed unused trace'; moved source cascading from scan.ML to source.ML; tuned;
2007-07-10 wenzelm 2007-07-10 moved print_mode setup for markup to markup.ML;
2007-07-10 wenzelm 2007-07-10 Markup.output;
2007-07-10 wenzelm 2007-07-10 use position.ML earlier;
2007-07-10 aspinall 2007-07-10 Add widthN to signature
2007-07-10 wenzelm 2007-07-10 cd ISABELLE_HOME/etc;
2007-07-10 haftmann 2007-07-10 adjusted
2007-07-10 haftmann 2007-07-10 updated keywords
2007-07-10 haftmann 2007-07-10 simplified, tuned
2007-07-10 haftmann 2007-07-10 re-expanded paths
2007-07-10 haftmann 2007-07-10 replaced code generator framework for reflected cooper
2007-07-10 haftmann 2007-07-10 expanded fragile proof
2007-07-10 haftmann 2007-07-10 extended - convers now basic lcm properties also
2007-07-10 haftmann 2007-07-10 constant dvd now in class target
2007-07-10 haftmann 2007-07-10 moved lemma zdvd_period here
2007-07-10 haftmann 2007-07-10 introduced (auxiliary) class dvd_mod for more convenient code generation
2007-07-10 wenzelm 2007-07-10 tuned;
2007-07-10 wenzelm 2007-07-10 nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-09 wenzelm 2007-07-09 tuned dead code;
2007-07-09 wenzelm 2007-07-09 use Position.file_of; removed strange comments;
2007-07-09 wenzelm 2007-07-09 toplevel_source: interactive flag indicates intermittent error_msg; nested source: error msg passed to recover; tuned source positions;
2007-07-09 wenzelm 2007-07-09 Malformed token: error msg; scan: explicit handling of malformed symbols from previous stage; source: interactive flag indicates intermittent error_msg; tuned;
2007-07-09 wenzelm 2007-07-09 adapted OuterLex/T.source;
2007-07-09 wenzelm 2007-07-09 scan: changed treatment of malformed symbols, passed to next stage; tuned sym_explode;
2007-07-09 wenzelm 2007-07-09 nested source: error msg passed to recover;
2007-07-09 wenzelm 2007-07-09 tuned signature; nested source: error msg passed to recover;
2007-07-09 wenzelm 2007-07-09 replaced name by file (unquoted); str_of: markup; misc cleanup;
2007-07-09 wenzelm 2007-07-09 moved Path.position to Position.path;
2007-07-09 wenzelm 2007-07-09 proper position markup; added properties operation; tuned;
2007-07-09 wenzelm 2007-07-09 use position.ML after pretty.ML;
2007-07-09 wenzelm 2007-07-09 removed target RAW-ProofGeneral (impractical to maintain);
2007-07-09 wenzelm 2007-07-09 declare: disallow quote (") in names;
2007-07-09 wenzelm 2007-07-09 removed legacy ML file; fixed prems_conv;
2007-07-09 wenzelm 2007-07-09 HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-09 obua 2007-07-09 adopted to new computing oracle and fixed bugs introduced by tuning
2007-07-09 obua 2007-07-09 added computing oracle support for HOL and numerals
2007-07-09 obua 2007-07-09 new version of computing oracle
2007-07-09 wenzelm 2007-07-09 simplified writeln_fn;
2007-07-09 wenzelm 2007-07-09 prompt: plain string, not output;
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-08 wenzelm 2007-07-08 symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08 wenzelm 2007-07-08 tuned;
2007-07-08 wenzelm 2007-07-08 thm tag: Markup.property list;
2007-07-08 wenzelm 2007-07-08 gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-08 wenzelm 2007-07-08 attribute tagged: single argument;
2007-07-08 wenzelm 2007-07-08 updated;
2007-07-08 wenzelm 2007-07-08 simplified Symtab;
2007-07-08 wenzelm 2007-07-08 renamed ML_exc to ML_exn;
2007-07-08 chaieb 2007-07-08 Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;