2003-10-09 skalberg 2003-10-09 Added info on the new 'finalconsts' command.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-10-08 skalberg 2003-10-08 Added axiomatic specifications (ax_specification).
2003-10-08 paulson 2003-10-08 now accepts DOS and Mac line breaks
2003-10-08 paulson 2003-10-08 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
2003-10-03 paulson 2003-10-03 added a comment
2003-10-02 paulson 2003-10-02 removal of junk and improvement of the document
2003-10-01 berghofe 2003-10-01 Fixed inefficiency in post_definition by adding weak case congruence rules to simpset.
2003-09-30 ballarin 2003-09-30 Removed garbage accidentally left behind in file.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed.
2003-09-30 ballarin 2003-09-30 Changed order of prems in finprod_cong. Slight speedup.
2003-09-30 ballarin 2003-09-30 Improvements wrt rule_tac.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-09-26 paulson 2003-09-26 new reference
2003-09-26 paulson 2003-09-26 tweak
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-26 paulson 2003-09-26 Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.
2003-09-26 paulson 2003-09-26 Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
2003-09-24 paulson 2003-09-24 new example for the Isar version of the ZF manual
2003-09-23 skalberg 2003-09-23 Fixed soundness bug.
2003-09-23 paulson 2003-09-23 conversion of NSP_Bad to Isar script
2003-09-23 paulson 2003-09-23 case_tac tweak
2003-09-23 paulson 2003-09-23 some basic new lemmas
2003-09-23 paulson 2003-09-23 Removal of the Key_supply axiom (affects many possbility proofs) and minor changes
2003-09-23 paulson 2003-09-23 new session HOL-SET-Protocol
2003-09-22 berghofe 2003-09-22 Modified merge_aux to prevent newer names from getting overwritten by older names.
2003-09-22 berghofe 2003-09-22 add_attribute now takes parser as argument.
2003-09-22 berghofe 2003-09-22 Added "del" attribute for deleting equations.
2003-09-22 berghofe 2003-09-22 Changed interface of add_attribute.
2003-09-22 berghofe 2003-09-22 Improved efficiency of code generated for functions int and nat.
2003-09-22 berghofe 2003-09-22 Improved efficiency of code generated for + and -
2003-09-22 berghofe 2003-09-22 Improved efficiency of code generated for < predicate on natural numbers.
2003-09-15 nipkow 2003-09-15 Mod due to new thm in Map.
2003-09-15 skalberg 2003-09-15 Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".
2003-09-15 skalberg 2003-09-15 Added the constant "curry".
2003-09-15 nipkow 2003-09-15 *** empty log message ***
2003-09-14 nipkow 2003-09-14 Added new theorems
2003-09-11 nipkow 2003-09-11 Added a number of thms about map restriction.
2003-09-04 berghofe 2003-09-04 Tried to make parser a bit more standard-conforming.
2003-09-04 berghofe 2003-09-04 Changed no_vars such that it outputs list of illegal schematic variables.
2003-09-04 paulson 2003-09-04 quantifier symbols
2003-09-04 paulson 2003-09-04 conversion of HOL/Auth/KerberosIV to new-style theory
2003-09-04 paulson 2003-09-04 new, separate specifications
2003-09-03 nipkow 2003-09-03 Introduced new syntax for maplets x |-> y
2003-09-01 paulson 2003-09-01 Corrections due to John Matthews
2003-08-31 skalberg 2003-08-31 Makes interactive proof scripting recognize the show_all_types flag.
2003-08-31 skalberg 2003-08-31 Added 'ambiguity_is_error' flag, which, if set, makes the parser fail, rather than just issue a warning, when the input parsed is ambiguous.
2003-08-29 skalberg 2003-08-29 Added show_all_types flag, such that all type information in the term is made explicit.
2003-08-29 ballarin 2003-08-29 Method rule_tac understands Isar contexts: documentation.
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Fixed typos.
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2003-08-27 skalberg 2003-08-27 Added skalberg to recepients, changed admin from kleing to berghofe.
2003-08-27 skalberg 2003-08-27 Converted to new style theories.
2003-08-27 skalberg 2003-08-27 Prepared for extended identifiers (\<alpha>, etc.)
2003-08-27 skalberg 2003-08-27 Improved the error messages (slightly).
2003-08-26 skalberg 2003-08-26 Cleaned up the code.
2003-08-26 skalberg 2003-08-26 New specification syntax added (the specification may be split over several properties).