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.
2007-07-11 berghofe 2007-07-11 Added function norm_proof for normalizing the proof term corresponding to a theorem.
2007-07-11 berghofe 2007-07-11 Added function rew_proof (for pre-normalizing proofs).
2007-07-11 berghofe 2007-07-11 Function unify_consts moved from OldInductivePackage to PrimrecPackage.
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-07-11 berghofe 2007-07-11 Renamed accessible part for predicates to accp.
2007-07-11 berghofe 2007-07-11 renamed inductive2 to inductive.
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-07-11 berghofe 2007-07-11 Hide member constant.
2007-07-11 berghofe 2007-07-11 Reverted renaming of "member".
2007-07-11 obua 2007-07-11 changed sources for HOL-Complex-Matrix
2007-07-11 berghofe 2007-07-11 Restored set notation in Multiset theory.
2007-07-11 obua 2007-07-11 added dummy makestring function
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-07-11 obua 2007-07-11 fixed for SML/NJ
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-07-11 berghofe 2007-07-11 Adapted to changes in Accessible_Part theory.
2007-07-11 berghofe 2007-07-11 Function unify_consts moved from OldInductivePackage to PrimrecPackage.
2007-07-11 berghofe 2007-07-11 New wrapper for defining inductive sets with new inductive predicate package.
2007-07-11 berghofe 2007-07-11 Old (co)inductive command is now replaced by (co)inductive_set.
2007-07-11 berghofe 2007-07-11 Reorganization due to introduction of inductive_set wrapper.
2007-07-11 berghofe 2007-07-11 Improved code generator for Collect.
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-07-11 aspinall 2007-07-11 Fix nested PGIP messages. Update for schema simplifications.
2007-07-11 berghofe 2007-07-11 Moved unify_consts to PrimrecPackage.
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-07-11 berghofe 2007-07-11 Adapted to changes in Predicate theory.