\begin{thebibliography}{99}

\bibitem[Age97]{agfr} Sten Agerholm \& Jacob Frost, 
An Isabelle-Based Theorem Prover for VDM-SL,
in Proceedings of TPHOLs'97,
Lecture Notes in Computer Science 1275 (1997), 1--16.

\bibitem[BCJ84]{BCJ} H. Barringer, J.H. Cheng \& C.B. Jones,
A Logic Covering Undefinedness in Program Proofs,
Acta Informatica 21 (1984), 251--269.

\bibitem[Bel82]{Bel} Nuel D. Belnap, Display Logic,
Journal of Philosophical Logic 11 (1982), 375--417.

\bibitem[Bli88]{Blikle} A. Blikle,
Three-valued predicates for software specification and validation,
in R. Bloomfield, L. Marshall \& R. Jones, VDM --- The Way Ahead, 
Lecture Notes in Computer Science 328 (1988), 243--266.

\bibitem[ChJ91]{CJ} J.H. Cheng \& C.B. Jones,
On the usability of logics which handle partial functions,
in Proceedings of the 3rd Refinement Workshop,
ed. C. Morgan \& J.C.P. Woodcock, Springer-Verlag (1991), 51--69.

\bibitem[Daw97]{thesis} Jeremy E. Dawson,
Mechanised Proof Systems for Relation Algebras,
Grad.\ Dip.\ Sci.\ sub-thesis, Dept of Computer Science,
Australian National University.  Available at
\verb|http://arp.anu.edu.au:80/~jeremy/thesis.dvi|

\bibitem[Dun91]{Dunn} J.M. Dunn,
{Gaggle theory: An abstraction of {G}alois connections
and residuation with applications to negation and various logical operations},
in Proceedings of JELIA 1990,
Lecture Notes in Computer Science 478 (1991), 31--51.

%@InProceedings{dunn-gaggle-theory,
  %author =       {J M Dunn},
  %title =        {Gaggle theory: An abstraction of {G}alois connections
                  %and residuation with applications to negation and
                  %various logical operations},
  %booktitle =    {JELIA 1990: Proceedings of the European Workshop on Logics in
                  %Artificial Intelligence},
  %volume =       {LNCS 478},
  %year =         1991,
  %publisher =    {Springer}

\bibitem[EOC97]{dove} K.A.Easthaughffe, M.A.Ozols and A.Cant,
Proof Tactics for a Theory of State Machines in a Graphical Environment,
in Proceedings of CADE-14, Lecture Notes in Computer Science 1249 (1997),
366--379.

\bibitem[HOL91]{HOLdesc} The HOL System Description, Version 2,
Computer Laboratory, Cambridge, 1991.

\bibitem[Gor95a]{sdpr} Rajeev Gor\'e,
Solving the Display Problem by Residuation, 
Automated Reasoning Project TR-ARP-12-95, ANU, 1995.

\bibitem[Gor95b]{ILR} Rajeev Gor\'e, Intuitionistic Logic Redisplayed, 
Automated Reasoning Project TR-ARP-1-95, ANU, 1995.

\bibitem[Gor97]{dRA} Rajeev Gor\'e, 
Cut-free Display Calculi for Relation Algebras,
Computer Science Logic, Lecture Notes in Computer Science 1249 (1997), 198--210.
%(or see \verb'http://arp.anu.edu.au/~rpg/publications.html').

\bibitem[Gag91]{LP} Stephen J. Garland \& John V. Guttag,
A Guide to LP, the Larch Prover,
SRC Research Report 82,
Digital Equipment Corporation, Palo Alto, 1991.

\bibitem[Gru96]{jgwi} Jim Grundy,
Transformational Hierarchical Reasoning,
The Computer Journal 39 (1996), 291--302.

\bibitem[Gru91]{jgwimp} Jim Grundy,
Window Inference in the HOL system,
in Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds),
Proc. International Work on the HOL theorem Proving System and its
Applications, IEEE COmputer Society Press, 1991, 177--189.

\bibitem[Jon96]{TANSTAAFL} C. B. Jones, 
{TANSTAAFL} with partial functions,
in Proceedings of the Workshop on the Mechanization Of Partial Functions,
ed. William Farmer, Manfred Kerber \& Michael Kohlhase (1996), 53--64.

\bibitem[Man74]{Manna} Zohar Manna,
Mathematical Theory of Computation, McGraw-Hill, 1974.

%\bibitem{Int} Lawrence C. Paulson,
%Introduction to Isabelle,
%Computer Laboratory, University of Cambridge, 1995.

\bibitem[Pau95]{Ref} Lawrence C. Paulson,
The Isabelle Reference Manual,
Computer Laboratory, University of Cambridge, 1995.

%\bibitem{OL} Lawrence C. Paulson,
%Isabelle's Object-Logics,
%Computer Laboratory, University of Cambridge, 1995.

\bibitem[Rea89]{Reade} Chris Reade,
Elements of Functional Programming, Addison-Wesley, 1989.

\bibitem[RoS93]{wi}
Peter J. Robinson \& John Staples,
Formalizing a Hierarchical Structure of Practical Mathematical Reasoning,
J. Logic \& Computation, 3 (1993), 47--61.

\bibitem[Wan94]{Wansing} Heinrich Wansing,
Sequent Calculi for Normal Modal Propositional Logics,
Journal of Logic and Computation 4 (1994), 124--142. 

\end{thebibliography}