2003-10-17 paulson 2003-10-17 Prevent recdef from looping when the inductio rule is simplified
2003-10-17 paulson 2003-10-17 improved tracing
2003-10-16 paulson 2003-10-16 partial conversion to Isar scripts
2003-10-16 paulson 2003-10-16 improved presentation
2003-10-16 paulson 2003-10-16 line-breaks; rewording
2003-10-16 paulson 2003-10-16 partial conversion to Isar scripts
2003-10-15 berghofe 2003-10-15 Fixed bug in mk_ind_def that caused the inductive definition package to crash in cases where the declaration of a constant and its definition were located in different theory files.
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 allow \<^sub> in identifiers
2003-10-15 kleing 2003-10-15 included \<^sub> in the range of identifier chars
2003-10-13 skalberg 2003-10-13 Fixed spelling error.
2003-10-10 berghofe 2003-10-10 Added overview page.
2003-10-10 berghofe 2003-10-10 Munich webserver is now atbroy1
2003-10-10 paulson 2003-10-10 trivial
2003-10-10 paulson 2003-10-10 finalconsts
2003-10-10 skalberg 2003-10-10 Made judgments automatically declared final.
2003-10-10 paulson 2003-10-10 better presentation
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