More examples.

Small changes.

Added typevarlist

replace sstac

Introduced qed_spec_mp.

Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'

renamed expand_typ to norm_typ

simplified bind_thm

new SML heap images are now removed

Modified datatype com. Added (part of) relative completeness proof for Hoare logic.

made Isabelle compatible with SML/NJ 1.09

expanded tabs

expanded tabs

expanded tabs

expanded tabs; incorporated Konrad's changes

expanded tabs; renamed subtype to typedef; incorporated Konrad's changes

expanded tabs

expanded tabs

renamed subtype.ML to typedef.ML

documented split_all_tac in HOL.

renamed subtype.ML to typedef.ML

fixed two little bugs

right-hard -> right-hand

Typo

fixed typo

expanded tabs

expanded tabs; removed commit() from ROOT.ML

expanded tabs

fixed typo

expanded tabs

inserted tabs again

expanded tabs

removed tabs

added facility to associate arbitrary data with theories

added absolute_path

changed the way simpsets and information about datatypes are stored

Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...

extended warning regarding MAKE_HTML databases

added warning for databases made with set MAKE_HTML

Added vcwp

Renamed letI to LetI (for consistency)

Added discussion of "let" and pattern-matching

Stylistic changes to discussion of pattern-matching

Added a verified verification-condition generator.

Ran expandshort

Now expands TABS as well

trivial updates

New version number

*** empty log message ***

added Lattice demo;

added this stuff;

improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);

added comments

beautified file_info a bit

fixed bug in file_info

Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.

simplified file_info by using System.filedate

removed reference to Nat thms in elim_rls.

Minor mod.

Polished proofs.

Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule.

Modified non-empty-types warning in HOL.

Reduced indentation; no change in function

Purely cosmetic changes

Updated comments for compression functions

Removed unfold:thm from signature INTR_ELIM and from the functor result. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store.

Now mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.

fixed indentation

New version of type sections and many small changes.

Note that unfold is not exported, that mutual_induct can be omitted (as the trivial theorem True), and comments on storage Also uses Datatype instead of Univ/Quniv as parent theory for lists, and omits quotes around types in theory files.

Added line breaks and other cosmetic changes

defined take/drop by induction over list rather than nat.

Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.

Addition of compression, that is, sharing. Uses refs and Symtab (binary search trees) to get reasonable speed. Types and terms can be compressed.

Commented the datatype declaration of thm. Declared compress: thm -> thm to copy a thm and maximize sharing in it. "ext_axms" now calls Term.compress_term so that stored axioms use sharing.

Removed obsolete alist_of and st_of_alist. Is now simply a structure instead of a functor.

"prep_const" now calls compress_type to ensure sharing among types of constants in theories.

"prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.

Now "standard" compresses theorems (for sharing). Also, rewrite_rule and rewrite_goals_rule check for the empty list of rewrites and do nothing in that case.

Now loads symtab.ML before term.ML. Functor > SymtabFun has been changed to the structure Symtab.

changed predicate flat to is_flat in theory Fix.thy

setting base_path is now optional

added automatic handling of wrongly set base_path

added subdir_of

added chmod and chgrp

init_html now makes sure that base_path contains a physical path and no symbolic links

Added Pelletier's problem 62, as corrected in AAR Newletter #31

renamed parents_of to parents_of_name to avoid name clash with function from thm.ML

layout

removed quotes from consts and syntax sections

Introduced Monad syntax Pat := Val; Cont

trivial, automatic changes

Changed div_termination -> diff_less Corrected if_...

Improved error message, suggesting addition of type constraints if occurrences of the recursive set remain in the fixedpoint definition.

Now def of apfst uses pattern-matching

improved indentation

New function read_cterms is a combination of read_def_cterm and read_cterm. It reads and simultaneously type-checks a list of strings. cterm_of no longer catches exception TYPE; instead it must be caught later on and a message printed using Sign.exn_type_msg. More informative messages can be printed this way.

exports exn_type_msg for error messages. Calls new infer_types. Improved comments.

infer_types now takes a term list and a type list as argument. It is defined using the new function infer_terms. Error messages and comments also improved.

type_of1: improved error messages

Commented and renamed vars in readtm

removed quotes from consts and syntax sections

removed quotes from consts and syntax sections

removed quotes from syntax and consts sections

fixed bug: cur_thyname was overwritten because of early assignment

changed typeDecl

removed quotes from types section

added const_type to type_decl

corrected diagrams for type and simpleType

removed some more quotes

changed HTML documentation

modified simpleType

removed debugging message; link to non-existing super index is now omitted silently

simplified parser for constType

removed quotes from consts and syntax sections

removed spaghetti diagrams for constType

removed quotes from consts and syntax sections

changed syntax diagrams according to quote-less consts and syntax section

added \label{sec:shell-scripts}

added type class to simple_type