# HG changeset patch # User wenzelm # Date 971904676 -7200 # Node ID 73b46b18c34858c5717deeedc35bda052cbe653f # Parent dd46544e259d8cff085df6522ca5f3ff247a24af "The Supplemental Isabelle/HOL Library"; diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/Library.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Library.thy Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,9 @@ +(*<*) +theory Library = + Accessible_Part + + Multiset + + Quotient + + While_Combinator + While_Combinator_Example: + +end +(*>*) diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/README.html Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,114 @@ + + + + +HOL-Library/README + + + +

HOL-Library: supplemental theories for main Isabelle/HOL

+ +This is a collection of generic theories that may be used together +with main Isabelle/HOL. Note that theory loader path already includes +this directory by default. + +

+ +Addition of new theories should be done with some care, as the +``module system'' of Isabelle is rather simplistic. The following +guidelines may be helpful to achieve maximum re-usability and minimum +clashes with existing developments. + +

+ +
Files +
Avoid unnecessary scattering of theories over several files. Use +new-style theories only, as old ones tend to clutter the file space +with separate .thy and .ML files. + +
Examples + +
Theories should be as ``generic'' as is sensible. Unused (or +rather unusable?) standalone theories should be avoided; common +applications should actually refer to the present theory. Small +example uses may be included as well, but should be put in a separate +theory, such as Foobar accompanied by +Foobar_Examples. + +
Theory names +
The theory loader name space is flat, so use sufficiently +long and descriptive names to reduce the danger of clashes with the +user's own theories. The convention for theory names is as follows: +Foobar_Doobar (this looks best in LaTeX output). + +
Names of logical items +
There are separate hierarchically structured name spaces for +types, constants, theorems etc. Nevertheless, some care should be +taken, as the name spaces are always ``open''. Use adequate names; +avoid unreadable abbreviations. The general naming convention is to +separate word constituents by underscores, as in foo_bar or +Foo_Bar (this looks best in LaTeX output). + +

+ +Note that syntax is global; qualified names loose syntax on +output. Do not use ``exotic'' symbols for syntax (such as +\<oplus>), but leave these for user applications. + +

Global context declarations +
Only items introduced in the present theory should be declared +globally (e.g. as Simplifier rules). Note that adding / deleting +rules stemming from parent theories may result in strange behavior +later, depending on the user's arrangement of import lists. + +
Mathematical symbols +
Non-ASCII symbols should be used with some care. In particular, +avoid unreadable arrows: ==> should be preferred over +\<Longrightarrow>. Use isatool unsymbolize to +clean up the sources. + +

+ +The following ASCII symbols of HOL should be generally avoided: +@, !, ?, ?!, %, better +use SOME, ALL (or \<forall>), +EX (or \<exists>), EX! (or +\<exists;>!), \<lambda>, respectively. +Note that bracket notation [| |] looks bad in LaTeX +output. + +

+ +Some additional mathematical symbols are quite suitable for both +readable sources and output document: +\<Inter>, +\<Union>, +\<and>, +\<in>, +\<inter>, +\<not>, +\<noteq>, +\<notin>, +\<or>, +\<subset>, +\<subseteq>, +\<times>, +\<union>. + +

Spacing + +
Isabelle is able to produce a high-quality LaTeX document from the +theory sources, provided some minor issues are taken care of. In +particular, spacing and line breaks are directly taken from source +text. Incidently, output looks very good common type-setting +conventions are observed: put a single space after each +punctuation character (",", ".", etc.), but none +before it; do not extra spaces inside of parentheses, unless the +delimiters are composed of multiple symbols (as in +[| |]); do not attempt to simulate table markup with +spaces, avoid ``hanging'' indentations. + +
+ + + diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ROOT.ML Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,2 @@ + +use_thy "Library"; diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/document/root.bib Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,27 @@ + +@InProceedings{Slotosch:1997, + author = {Oscar Slotosch}, + title = {FIXME}, + crossref = {tphols97}} + +@InProceedings{paulin-tlca, + author = {Christine Paulin-Mohring}, + title = {Inductive Definitions in the System {Coq}: Rules and + Properties}, + crossref = {tlca93}, + pages = {328-345}} + +@Proceedings{tlca93, + title = {Typed Lambda Calculi and Applications}, + booktitle = {Typed Lambda Calculi and Applications}, + editor = {M. Bezem and J.F. Groote}, + year = 1993, + publisher = {Springer}, + series = {LNCS 664}} + +@Proceedings{tphols97, + title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, + booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, + editor = {Elsa L. Gunter and Amy Felty}, + series = {LNCS 1275}, + year = 1997} diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/document/root.tex Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,42 @@ + +% $Id$ + +\documentclass[11pt,a4paper]{article} +\usepackage{ifthen} +\usepackage{isabelle,isabellesym,pdfsetup} + +\urlstyle{rm} +\isabellestyle{it} +\pagestyle{myheadings} + +\begin{document} + +\title{The Supplemental Isabelle/HOL Library} +\author{ + Gertrud Bauer \\ + Tobias Nipkow \\ + Lawrence C Paulson \\ + Markus Wenzel} +\maketitle + +\tableofcontents +\newpage + +%now hack the "header" markup to support \title and \author +\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}} +\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}} +\renewcommand{\isamarkupheader}[1]% +{\newpage\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1% +\markright{THEORY~``\isabellecontext''} +\ifthenelse{\equal{}{\isabelletitle}}{}{\section{\isabelletitle}}% +\ifthenelse{\equal{}{\isabelleauthor}}{}% +{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}} + +\parindent 0pt \parskip 0.5ex +\input{session} + +\pagestyle{headings} +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}