Added an equivalence proof which avoids the use of -n-> (with help from Ranan Fraer)

Added backwards rtrancl_induct and special versions for pairs.

changed ident_no_colon so that it forbids postfix "=", too

changed use_thy's behaviour so that if the user specifies a path for a theory the loadpath is temporarily expanded while the ancestors are loaded

moved dest_cimplies to drule.ML; added adjust_maxidx

Cosmetic re-ordering of declarations

Streamlined syntax: -(n)-> is now -n->.

Natural and Transition semantics.

Forgot to add Expr to IMP.

Updated IMP

Arithemtic and boolean expressions are now in a separate theory. The commands don not use them directly. Instead they are based on the semantics (rather than the syntax) of expressions.

A completely new version of IMP.

Generalized types of some of the operators (thanks to Norbert Voelker)

Added R_O_id and id_O_R

Added R^1 = R

Renaming of a lemma

Fixed indenting

added changes by Konrad to prove_nchotomy

Fixed some unfortunate variable names

Now contains HOLCF

temporarily included settings for unification bounds again

Added functions mk_cntxt_splitthm and inst_split which instantiate the split-rule before it is applied. Inserted some comments.

Fixed a silly variable name

Rearrangement and polishing to look for for publication

Now calls "rail" to update datatype syntax charts

automatic updates

changed two goals formulated with 8bit font

removed David's private version (i.e. restored version 1.1)

*** empty log message ***

*** empty log message ***

repaired critical proofs depending on the order inside non-confluent SimpSets,

*** empty log message ***

adapted several proofs

*** empty log message ***

repaired critical proofs depending on the order inside non-confluent SimpSets

repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"

included (empty) test goal for symmetry reasons

use_dir and exit_use_dir now change the CWD only temporarily

inserted Suc_less_eq explictly in a few proofs. inserted o_def explictly in a few proofs because the new split_tac causes fewer eta-expansions which some of the rewrites need. Indented proof in I.ML

added Konrad's code for the datatype package

adapted to new version of Fun.ML

removed assignment of HOL_ss to simpset

added thy_data.ML

added thyname_of_sign (used in HOL/thy_data.ML)

adapted proof of drop_succ_Cons: problem with non-confluent simpset removed

adapted proof of less_succ: problem because of non-confluent SimpSet removed

*** empty log message ***

*** empty log message ***

*** empty log message ***

add_thydata and get_thydata now take a string as their first argument

changed first parameter of add_thydata and get_thydata

fixed bug in set_current_thy

Added a number of lemmas

select_match now sorts list of matching theorems according to the number of premises and size of the required substitution

Replaced !simpset by HOL_ss on line 93.

Proved Inter_0 and converse_INT

deleted obsolete comment

Added 'constdefs'

Added 'constdefs' and extended the section on 'defs'

Messed up last update.

Replaced \CHOL by \HOLCF

updated comments

Moved link to paper.

Removed 8bit characters used by mistake

Fixed error in CHANGED (caused by variable renaming)

Using new "Times" infix

For renaming to rtrancl_Un_rtrancl

Added more _iff rewrites for Compl, Un, Int

New example Comb: Church-Rosser for combinators, ported from ZF

*** empty log message ***

Updated: 01-Mar-96 when functional strictified, copy_def based on when_def

Introduced Times and SIGMA.

*** empty log message ***

Plugged some more loopholes with nodup_Vars.

Simplified proof of tiling_UnI

Binary integers and their numeric syntax

new lemma for mutilated chess board

Simplified proof of tiling_UnI

Mended indentation

Added functions pr_latex and printgoal_latex which display current proof state in xdvi window

Optimized type inference (avoids chains of the form 'a |-> 'b |-> 'c ... in tye)

Moved even/odd lemmas from ex/Mutil to Arith

Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy

Alternative proof removes dependence upon AC

Ran expandshort

New theorem Finite_imp_succ_cardinal_Diff

New mutilated checkerboard example

Added Mutil to ex targets

Now use _irrefl instead of _anti_refl

Library changes for mutilated checkerboard

Simplified proofs, esp. for new ZF_ss

Moved some proofs to Cardinal.ML; simplified others

Moved some proofs to FOL/IFOL.ML

Rewriting changes due to new arith_ss

Now loads Mutil example

Added new rewrite rules about cons and succ

New results from AC/Cardinal_aux.ML

Updated comments

New lemmas for Mutilated Checkerboard

Added two of KGs rules

New example file: Mutil

New example: mutilated checkerboard

added converse_converse

replaced "rules" by "primrec"

moved init_data to new public function set_current_thy

fixed incompatibility of add_to_parents with SML109's new Io exceptions

Changes required by removal of the theory argument of Theorem

Examples call gocls to make goal clauses

Now labels the Horn and goal clauses to make the proof objects more readable

For the new version of name_thm. Now the same theorem is stored as is returned, as both contain a label and a link to the previous derivation. So get_thm no longer needs to attach a label to its resulting theorem.

name_thm no longer takes a theory argument, as the name no longer hides the previous derivation. Deleted sign_of_thm as redundant.

Printing & string functions moved to display.ML

Now loads deriv.ML

Includes deriv.ML and display.ML as dependencies

New module for proof objects (deriviations)

maketest now closes the output file Declared type mtree for proof objects

New module for display/printing operations, taken from drule.ML

Describes proof objects and Deriv module

added warning and automatic deactivation of HTML generation if we cannot write .theory_list.txt; fixed bug which occured when index_path's value is "/"

New file containing search tacticals