2004-06-08 berghofe 2004-06-08 add_dummies no longer uses transform_error but handles specific exception Datatype_Empty instead.
2004-06-08 berghofe 2004-06-08 Added exception Datatype_Empty.
2004-06-08 berghofe 2004-06-08 mk_id is now also applied to identifiers in test_term.
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas in ZF
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas
2004-06-06 wenzelm 2004-06-06 avoid Args.list (lost update?);
2004-06-06 wenzelm 2004-06-06 added has_mode; handle_error: output raw;
2004-06-06 wenzelm 2004-06-06 Symbol.output;
2004-06-06 wenzelm 2004-06-06 no token translation / setup for Latex;
2004-06-06 wenzelm 2004-06-06 HOL: symbolic syntax of Eps;
2004-06-05 chaieb 2004-06-05 More readable code.
2004-06-05 wenzelm 2004-06-05 pretty_thm/goals_aux, pretty_flexpair: pp;
2004-06-05 wenzelm 2004-06-05 avoid implicit arguments via refs;
2004-06-05 wenzelm 2004-06-05 Symbol.decode;
2004-06-05 wenzelm 2004-06-05 added datatype sym, val decode: symbol -> sym;
2004-06-05 wenzelm 2004-06-05 improved symbolic syntax of Eps: \<some> for mode "epsilon";
2004-06-05 wenzelm 2004-06-05 removed mlworks and smlnj-0.93 (obsolete);
2004-06-05 wenzelm 2004-06-05 tuned comments;
2004-06-05 wenzelm 2004-06-05 moved exception handling back to library.ML;
2004-06-05 wenzelm 2004-06-05 tuned exeption handling (capture/release);
2004-06-05 wenzelm 2004-06-05 removed Pure/ML-Systems/mlworks.ML Pure/ML-Systems/polyml-3.x.ML Pure/ML-Systems/smlnj-0.93.ML; added ML-Systems/polyml-time-limit.ML;
2004-06-05 wenzelm 2004-06-05 obsolete;
2004-06-04 berghofe 2004-06-04 Tuned parse_att.
2004-06-02 paulson 2004-06-02 new rules for simplifying quantifiers with Sigma
2004-06-01 aspinall 2004-06-01 Add alternative syntax for attributes
2004-06-01 aspinall 2004-06-01 Add panic function which exits Isabelle immediately.
2004-06-01 berghofe 2004-06-01 Removed ~10000 hack in function idx that can lead to inconsistencies when unifying terms with a large number of abstractions.
2004-06-01 berghofe 2004-06-01 Adapted to new name mangling function in code generator.
2004-06-01 berghofe 2004-06-01 Adapted to new name mangling function.
2004-06-01 berghofe 2004-06-01 Improved name mangling function.
2004-06-01 wenzelm 2004-06-01 proper use of 'nonterminals';
2004-06-01 wenzelm 2004-06-01 proper treatment of logical types within syntax;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic' and '=?=' syntax;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-06-01 paulson 2004-06-01 more on bij_betw
2004-06-01 paulson 2004-06-01 tidied
2004-06-01 webertj 2004-06-01 TimeLimit structure added (no proper implementation yet)
2004-06-01 webertj 2004-06-01 including polyml-time-limit.ML
2004-06-01 webertj 2004-06-01 SML/NJs TimeLimit structure ported to Poly/ML
2004-05-31 wenzelm 2004-05-31 oops -- no Output.out here;
2004-05-29 wenzelm 2004-05-29 updated;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29 wenzelm 2004-05-29 Scan.this; tuned;
2004-05-29 wenzelm 2004-05-29 do *not* export list/list1 -- commas considered special in arg syntax;
2004-05-29 wenzelm 2004-05-29 target 'generate';
2004-05-29 wenzelm 2004-05-29 avoid Args.list;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
2004-05-29 wenzelm 2004-05-29 tuned _dummy_ofsort syntax;
2004-05-29 wenzelm 2004-05-29 added pp_show_brackets; support unbreakable blocks;
2004-05-29 wenzelm 2004-05-29 transform_error;
2004-05-29 wenzelm 2004-05-29 Library.read_int; Output.output;
2004-05-29 wenzelm 2004-05-29 improved support for raw symbols;
2004-05-29 wenzelm 2004-05-29 Output.error;
2004-05-29 wenzelm 2004-05-29 pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
2004-05-29 wenzelm 2004-05-29 added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
2004-05-29 wenzelm 2004-05-29 removed norm_typ; improved output; refer to Pretty.pp;
2004-05-29 wenzelm 2004-05-29 moved read_int etc. to library.ML; added type 'arity';