diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Package/Ind_Intro.thy
--- a/CookBook/Package/Ind_Intro.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-theory Ind_Intro
-imports Main 
-begin
-
-chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}
-
-text {*
-  \begin{flushright}
-  {\em
-  ``My thesis is that programming is not at the bottom of the intellectual \\
-  pyramid, but at the top. It's creative design of the highest order. It \\
-  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
-  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
-  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
-  \end{flushright}
-
-  \medskip
-  HOL is based on just a few primitive constants, like equality and
-  implication, whose properties are described by axioms. All other concepts,
-  such as inductive predicates, datatypes, or recursive functions have to be defined
-  in terms of those constants, and the desired properties, for example
-  induction theorems, or recursion equations have to be derived from the definitions
-  by a formal proof. Since it would be very tedious for a user to define
-  complex inductive predicates or datatypes ``by hand'' just using the
-  primitive operators of higher order logic, \emph{definitional packages} have
-  been implemented automating such work. Thanks to those packages, the user
-  can give a high-level specification, for example a list of introduction
-  rules or constructors, and the package then does all the low-level
-  definitions and proofs behind the scenes. In this chapter we explain how
-  such a package can be implemented.
-
-  As a running example, we have chosen a rather simple package for defining
-  inductive predicates. To keep things really simple, we will not use the
-  general Knaster-Tarski fixpoint theorem on complete lattices, which forms
-  the basis of Isabelle's standard inductive definition package.  Instead, we
-  will use a simpler \emph{impredicative} (i.e.\ involving quantification on
-  predicate variables) encoding of inductive predicates. Due to its
-  simplicity, this package will necessarily have a reduced functionality. It
-  does neither support introduction rules involving arbitrary monotone
-  operators, nor does it prove case analysis (or inversion) rules. Moreover,
-  it only proves a weaker form of the induction principle for inductive
-  predicates.
-*}
-
-end