2001-09-26 wenzelm 2001-09-26 use darkblue for all links;
2001-09-26 wenzelm 2001-09-26 updated;
2001-09-25 wenzelm 2001-09-25 updated;
2001-09-25 wenzelm 2001-09-25 *** empty log message ***
2001-09-25 wenzelm 2001-09-25 tuned;
2001-09-21 oheimb 2001-09-21 Minor improvements, added Example
2001-09-17 wenzelm 2001-09-17 tuned;
2001-09-13 berghofe 2001-09-13 Fixed proof term bug in permute_prems.
2001-09-12 wenzelm 2001-09-12 result_error_default: include msg;
2001-09-11 nipkow 2001-09-11 *** empty log message ***
2001-09-10 oheimb 2001-09-10 marginally improved comments
2001-09-10 oheimb 2001-09-10 corrected antiquotations in comment
2001-09-10 oheimb 2001-09-10 simplified vnam/vname, introduced fname, improved comments
2001-09-10 wenzelm 2001-09-10 tuned usage;
2001-09-08 wenzelm 2001-09-08 print_state: subgoals;
2001-09-08 wenzelm 2001-09-08 export pretty_goals;
2001-09-08 wenzelm 2001-09-08 result_error_default: output *single* error message;
2001-09-08 wenzelm 2001-09-08 tuned;
2001-09-08 wenzelm 2001-09-08 ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);
2001-09-08 wenzelm 2001-09-08 * system: support Poly/ML 4.1.1 (large heaps); * system: smart selection of Isabelle process versus Isabelle interface, accomodates case-insensitive file systems (e.g. HFS+);
2001-09-08 wenzelm 2001-09-08 smart selection of isabelle-process versus isabelle-interface;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-09-04 nipkow 2001-09-04 *** empty log message ***
2001-09-03 nipkow 2001-09-03 *** empty log message ***
2001-09-01 wenzelm 2001-09-01 tuned;
2001-09-01 wenzelm 2001-09-01 final proofs := 0;
2001-09-01 wenzelm 2001-09-01 HOL-Real-Hyperreal made a plain session (no longer an image);
2001-09-01 wenzelm 2001-09-01 renamed `keep_derivs' to `proofs', and made an integer;
2001-08-31 wenzelm 2001-08-31 * Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el);
2001-08-31 wenzelm 2001-08-31 proper use of invent_names;
2001-08-31 wenzelm 2001-08-31 fixed header;
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-31 wenzelm 2001-08-31 keyword classification tables for Isabelle/Isar Proof General (generated by ProofGeneral.write_keywords from Isabelle/HOLCF/IOA);
2001-08-31 berghofe 2001-08-31 New code generators for HOL.
2001-08-31 berghofe 2001-08-31 Initial revision of tools for proof terms.
2001-08-31 berghofe 2001-08-31 Added new option for setting level of detail for proof objects.
2001-08-31 berghofe 2001-08-31 Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.
2001-08-31 berghofe 2001-08-31 Added code generator setup.
2001-08-31 berghofe 2001-08-31 Added new files for code generator.
2001-08-31 berghofe 2001-08-31 Renamed functions % and %% to avoid clash with syntax for proof terms.
2001-08-31 berghofe 2001-08-31 Adapted to new proof terms.
2001-08-31 berghofe 2001-08-31 Exported ml_reserved.
2001-08-31 berghofe 2001-08-31 Made consts list operations a bit faster.
2001-08-31 berghofe 2001-08-31 Added new argument to use_dir for derivation kind.
2001-08-31 berghofe 2001-08-31 Removed tag_assumption.
2001-08-31 berghofe 2001-08-31 Tuned naming of theorems.
2001-08-31 berghofe 2001-08-31 Added functions for printing primitive proof terms.
2001-08-31 berghofe 2001-08-31 Tuned function extend_lexicon.
2001-08-31 berghofe 2001-08-31 Initial revision of tools for proof terms.
2001-08-31 berghofe 2001-08-31 Now obsolete; replaced by LF style proof terms.
2001-08-31 berghofe 2001-08-31 Initial version of generic code generator.
2001-08-31 berghofe 2001-08-31 New implementation of LF style proof terms.
2001-08-31 berghofe 2001-08-31 Replaced old derivations by proof terms.
2001-08-31 berghofe 2001-08-31 Tidied function SELECT_GOAL.
2001-08-31 berghofe 2001-08-31 Added equality axioms and initialization of proof term package.
2001-08-31 berghofe 2001-08-31 Added setup for code generator.
2001-08-31 berghofe 2001-08-31 Added function unique_strings.
2001-08-31 berghofe 2001-08-31 - exported SAME exception - exported functions for normalizing types
2001-08-31 berghofe 2001-08-31 Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms.
2001-08-31 berghofe 2001-08-31 Added new files for proof terms.