2007-07-18 aspinall 2007-07-18 DEEPEN: Use priority message channel for interim messages (not warnings).
2007-07-18 aspinall 2007-07-18 Direct priority and tracing channels properly.
2007-07-18 paulson 2007-07-18 tidying using metis
2007-07-17 wenzelm 2007-07-17 fileident --- produce file identification based;
2007-07-17 wenzelm 2007-07-17 added ISABELLE_FILE_IDENT (command line for source file identification);
2007-07-17 wenzelm 2007-07-17 adapted TextIO.inputLine;
2007-07-17 wenzelm 2007-07-17 tuned comment;
2007-07-17 wenzelm 2007-07-17 avoid redundant variables in patterns (which made Alice vomit);
2007-07-17 paulson 2007-07-17 Full sort information by default. Race condition on successful proofs fixed.
2007-07-17 berghofe 2007-07-17 Added hypotheses.
2007-07-17 berghofe 2007-07-17 Added clause for hypotheses to proof_of_xml function.
2007-07-17 wenzelm 2007-07-17 use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
2007-07-17 krauss 2007-07-17 reverted fun->recdef, since there are problems with induction rule
2007-07-17 wenzelm 2007-07-17 Pure theory setup.
2007-07-17 wenzelm 2007-07-17 Generic print mode.
2007-07-17 wenzelm 2007-07-17 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-17 wenzelm 2007-07-17 simplified loading of ML files -- no static forward references;
2007-07-17 wenzelm 2007-07-17 moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-07-17 wenzelm 2007-07-17 added General/print_mode.ML, pure_setup.ML;
2007-07-17 wenzelm 2007-07-17 tuned specifications;
2007-07-16 krauss 2007-07-16 use function package
2007-07-16 krauss 2007-07-16 more proofs
2007-07-16 krauss 2007-07-16 some interface cleanup
2007-07-16 krauss 2007-07-16 added lemma binding: accpI = accp.accI
2007-07-16 krauss 2007-07-16 updated
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 paulson 2007-07-16 tidied
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 haftmann 2007-07-16 clarified structure names
2007-07-16 haftmann 2007-07-16 added function for case certificates
2007-07-16 haftmann 2007-07-16 dropped outer ROOT structure for generated code
2007-07-16 haftmann 2007-07-16 tuned
2007-07-16 haftmann 2007-07-16 fixed SML/NJ int problem
2007-07-16 haftmann 2007-07-16 updated
2007-07-13 wenzelm 2007-07-13 tuned;
2007-07-12 krauss 2007-07-12 updated
2007-07-12 wenzelm 2007-07-12 updated;
2007-07-12 wenzelm 2007-07-12 tuned signature; misc cleanup / simplification;
2007-07-12 wenzelm 2007-07-12 sys_error;
2007-07-12 wenzelm 2007-07-12 simplified using Markup.get_int; renamed PgipParser to OldPgipParser;
2007-07-12 wenzelm 2007-07-12 added skeleton for print_mode setup; removed unused stuff;
2007-07-12 wenzelm 2007-07-12 tuned spacing;
2007-07-12 wenzelm 2007-07-12 renamed PgipParser to OldPgipParser;
2007-07-12 wenzelm 2007-07-12 Parsing theory sources without execution (via keyword classification).
2007-07-12 wenzelm 2007-07-12 exported command_keyword; tuned;
2007-07-12 wenzelm 2007-07-12 command 'declare': proper thy_decl;
2007-07-12 wenzelm 2007-07-12 added get_string, get_int; tuned;
2007-07-12 wenzelm 2007-07-12 added ProofGeneral/pgip_parser.ML;
2007-07-11 wenzelm 2007-07-11 tuned error faces;
2007-07-11 nipkow 2007-07-11 tries to solve goal via TrueI
2007-07-11 wenzelm 2007-07-11 tuned markup;
2007-07-11 wenzelm 2007-07-11 replaced OuterLex.name_of by more sophisticated OuterLex.text_of;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols); replaced OuterLex.name_of by more sophisticated OuterLex.text_of; tuned;
2007-07-11 wenzelm 2007-07-11 Buffer.markup;
2007-07-11 wenzelm 2007-07-11 removed ident, space; added antiq; tuned;
2007-07-11 wenzelm 2007-07-11 added markup operation;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11 berghofe 2007-07-11 Added entry for new inductive definition package.
2007-07-11 berghofe 2007-07-11 Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions.