cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
<H2>HOL: Higher-Order Logic</H2>
This directory contains the ML sources of the Isabelle system for
Higher-Order Logic.<P>
There are several subdirectories with examples:
<DL>
<DT>ex
<DD>general examples
<DT>Auth
<DD>a new approach to verifying authentication protocols
<DT>IMP
<DD>mechanization of a large part of a semantics text by Glynn Winskel
<DT>Induct
<DD>examples of (co)inductive definitions
<DT>Integ
<DD>a theory of the integers including efficient integer calculations
<DT>IOA
<DD>extended example of Input/Output Automata
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus
<DT>Subst
<DD>subdirectory defining a theory of substitution and unification.
</DL>
Useful references on Higher-Order Logic:
<UL>
<LI> P. B. Andrews,<BR>
An Introduction to Mathematical Logic and Type Theory<BR>
(Academic Press, 1986).
<P>
<LI> A. Church,<BR>
A Formulation of the Simple Theory of Types<BR>
(Journal of Symbolic Logic, 1940).
<P>
<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
Introduction to HOL: A theorem proving environment for higher order logic<BR>
(Cambridge University Press, 1993).
<P>
<LI> J. Lambek and P. J. Scott,<BR>
Introduction to Higher Order Categorical Logic<BR>
(Cambridge University Press, 1986).
</UL>
</BODY></HTML>