2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
2003-10-31 kleing 2003-10-31 fixed
2003-10-31 kleing 2003-10-31 set isatool usedir to verbose by default
2003-10-30 paulson 2003-10-30 Got rid of the structure "Int", which was obsolete and which obscured the eponymous Basis Library structure
2003-10-29 berghofe 2003-10-29 Inserted additional checks in functions dest_prem and add_prod_factors, to allow side conditions of the form "x : S", where S is not an inductive set.
2003-10-29 paulson 2003-10-29 tidying
2003-10-29 berghofe 2003-10-29 Tuned proof of choice_eq.
2003-10-29 nipkow 2003-10-29 *** empty log message ***
2003-10-24 kleing 2003-10-24 added sydney unsw mirror. contact: me (gerwin.klein@nicta.com.au)
2003-10-22 paulson 2003-10-22 auto update
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions
2003-10-22 paulson 2003-10-22 recursion
2003-10-21 skalberg 2003-10-21 Added access to the mk_rews field (and friends).
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.