Now sets loadpath.

Gave tighter priorities to SUM and PROD to reduce ambiguities.

Gave tighter priorities to if, napply and the let-forms to reduce ambiguities.

Now sets eta_contract.

Added Id: line

generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)

replaced 'arities' by 'instance';

Simplified using pattern replacements. Added the AC example.

New example of AC Equivalences by Krzysztof Grabczewski

New example of AC Equivalences by Krzysztof Grabczewski

Tried the new addss in many proofs, and tidied others involving simplification.

Tried the new addss in a proof.

Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)

changed translation of _applC

changed pretty printing of applC

Added comment about why mem_irrefl should not be a safeE.

Tried the new addss in many proofs, and tidied others involving simplification.

Precedence of infixes is now 4 (just above that of :=)

Addition of wrappers for integration with the simplifier. New infixes setwrapper compwrapper addbefore addafter. New function getwrapper. The wrapper is a tactical that is applied to the step tactic. By default it is the identity. Using THEN one can cause other tactics to be tried before or after the step tactic. Other effects are possible using ORELSE, etc.

Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)

removed unnecessary parentheses from the generated rules

Simplification: used Logic.occs instead of mem add_term_frees

changed string scanner so that newlines ('\n') are allowed and ignored inside strings

changed syntax of datatype declarations (curried types for constructor parameters)

renamed theorem "apfst" to "apfst_conv" to avoid conflict with function apfst from Pure/library.ML

Corrected faulty reference to Hindley-Milner type inference

Added recursion equations for foldl to list_ss.

Modified If_def to avoid ambiguity.

changed syntax of tuples from <..., ...> to (..., ...)

fixed bug: parent theory wasn't loaded if .thy file was completly read before (regardless of the .ML file)

fixed bug: HOL_build_completed replaced by CHOL_build_completed

converted ex with curried function application

converted Subst with curried function application

changed syntax of Unity ("()" instead of "<>")

converted IOA with curried function application

changed syntax of "if"

fixed two severe bugs in calc_xrules and case_rule

Corrected a silly old bug in merge_tsigs. Rewrote a lot of Nimmermann's code.

Added a few thms to nat_ss and list_ss

Removed bugs which occurred due to new generation mechanism for type variables

Removed exception handlers, as they are now in ZF/Makefile.

removed print_msg parameter of infer_types

Now mentions Coind

Removed exception handlers, as they are now in ZF/Makefile.

Now calls exit_use instead of use, for prompt failure if errors are detected.

Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).

Now the "use" call has an exception handler, for prompt failure if errors are detected.

Now calls exit_use instead of use, for prompt failure if errors are detected.

Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.

added exit 1

Removed superfluous type constraint

Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.

Added type constraints to enforce correct choice of variable names.

Put freeze into the signature TACTIC for export

Removed "localize"; instead, proofs refer to their own assumptions.

Commented isof(c,t)

Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML

Replaced read by read_cterm.

Enforced partial evaluation of mk_case_split_tac.

Enforced partial evaluation of mk_case_split_tac

Added dependencies on files in Provers

Added pretty-printing coments

*** empty log message ***

*** empty log message ***

Hoare logic

Changed Univ to Datatype in parents

Replaced rules by defs. Also got rid of tyconstU by including TyConst in the datatype's universe

Replaced rules by defs

Got rid of exvarU and constU by including ExVar and Const in various datatype universes.

Deleted constQU, exvarQU, expQU by including Const, ExpVar, Exp in Value.thy's codatatype declaration.

Replaced rules by defs

Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.

Moved declaration of ~= to a syntax section

replaced Pure by ProtoPure

fixed a bug in infer_types/exn_type_msg

new version of HOL/Integ with curried function application

new version of HOL/IMP with curried function application

new version of HOL with curried function application

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

added declaration of syntactic const "_abs";

Added initial /bin/csh line and comments

No longer calls maketest; instead, the Makefile writes the file test.

Uses "suffix substitution" to shorten macro definitions.

Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.

New example by Jacob Frost, tidied by lcp

New example by Jacob Frost, tidied by lcp

Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.

Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)

Redefined functions to suppress redundant leading 0s and 1s

new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;

Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.

intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ

Updated comment about list_subset_univ and list_into_univ.

exit: new, for use in Makefiles

Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Proved zadd_left_commute and zmult_left_commute to define zadd_ac and zmult_ac. Deleted add_cong, add_kill and add_left_commute_kill as unused. Defined zadd_simps, zminus_simps, zmult_simps and added them to integ_ss.

New shell script for finding orphan .ML files (those with no .thy file)

added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)

added check "length ts > 1" before printing ambiguity warning in infer_types

Improved test for looping rewrite rules.

replaced pair_ss by prod_ss

Improved check for looping conditional rewrite rules.

ID for the file

ID for the file

'get ID update working'

CVS: CVS:

CVS:

added qed, qed_goal[w]

added specification of csh as script interpreter

simplified elimination of chain productions

binder: optional body pri now [bracketted];

improved read_xrules: patterns no longer read twice; tuned read_typ;

*** empty log message ***

instance: now automatically includes defs of current thy node as witnesses;

binder: optional body pri now [bracketted];

added documentation of pwd

renamed Sign.ambiguity_level to Syntax.ambiguity_level

moved ambiguity_level from sign.ML to Syntax/syntax.ML

moved ambiguity_level to Syntax/syntax.ML