tidied

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.

Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.

fixed

set isatool usedir to verbose by default

Got rid of the structure "Int", which was obsolete and which obscured the eponymous Basis Library structure

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.

tidying

Tuned proof of choice_eq.

*** empty log message ***

added sydney unsw mirror. contact: me (gerwin.klein@nicta.com.au)

auto update

InductiveInvariant_examples illustrates advanced recursive function definitions

recursion

Added access to the mk_rews field (and friends).

Prevent recdef from looping when the inductio rule is simplified

improved tracing

partial conversion to Isar scripts

improved presentation

line-breaks; rewording

partial conversion to Isar scripts

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.

use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)

allow \<^sub> in identifiers

included \<^sub> in the range of identifier chars

Fixed spelling error.

Added overview page.

Munich webserver is now atbroy1

trivial

finalconsts

Made judgments automatically declared final.

better presentation

Added info on the new 'finalconsts' command.

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).

Added axiomatic specifications (ax_specification).

now accepts DOS and Mac line breaks

Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy

added a comment

removal of junk and improvement of the document

Fixed inefficiency in post_definition by adding weak case congruence rules to simpset.

Removed garbage accidentally left behind in file.

Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".

Improvements to Isar/Locales: premises generated by "includes" elements changed.

Changed order of prems in finprod_cong. Slight speedup.

Improvements wrt rule_tac.

Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".

new reference

tweak

misc tidying

Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.

Tidying of SET's "possibility theorems" (removal of Key_supply_ax)

new example for the Isar version of the ZF manual

Fixed soundness bug.

conversion of NSP_Bad to Isar script

case_tac tweak

some basic new lemmas

Removal of the Key_supply axiom (affects many possbility proofs) and minor changes

new session HOL-SET-Protocol

Modified merge_aux to prevent newer names from getting overwritten by older names.

add_attribute now takes parser as argument.

Added "del" attribute for deleting equations.

Changed interface of add_attribute.

Improved efficiency of code generated for functions int and nat.

Improved efficiency of code generated for + and -

Improved efficiency of code generated for < predicate on natural numbers.

Mod due to new thm in Map.

Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".

Added the constant "curry".

*** empty log message ***

Added new theorems

Added a number of thms about map restriction.

Tried to make parser a bit more standard-conforming.

Changed no_vars such that it outputs list of illegal schematic variables.

quantifier symbols

conversion of HOL/Auth/KerberosIV to new-style theory

new, separate specifications

Introduced new syntax for maplets x |-> y

Corrections due to John Matthews

Makes interactive proof scripting recognize the show_all_types flag.

Added 'ambiguity_is_error' flag, which, if set, makes the parser fail, rather than just issue a warning, when the input parsed is ambiguous.

Added show_all_types flag, such that all type information in the term is made explicit.

Method rule_tac understands Isar contexts: documentation.

Methods rule_tac etc support static (Isar) contexts.

Removed the extended digits again.

Fixed typos.

Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.

Added skalberg to recepients, changed admin from kleing to berghofe.

Converted to new style theories.

Prepared for extended identifiers (\<alpha>, etc.)

Improved the error messages (slightly).

Cleaned up the code.

New specification syntax added (the specification may be split over several properties).

Allowed for splitting the specification over several lemmas.

Improved handling of modes for equality predicate, to avoid ill-typed ML code due to comparisons between elements of function types.

Fixed problem with "code ind" attribute that caused code generator to fail for mutually recursive predicates.

Added function strong_conn for computing the strongly connected components of the graph.