equal
deleted
inserted
replaced
1 theory Ind_Intro |
1 theory Ind_Intro |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 chapter {* How to Write a Definitional Package\label{chp:package} *} |
6 chapter \<open>How to Write a Definitional Package\label{chp:package}\<close> |
7 |
7 |
8 text {* |
8 text \<open> |
9 \begin{flushright} |
9 \begin{flushright} |
10 {\em |
10 {\em |
11 ``We will most likely never realize the full importance of painting the Tower,\\ |
11 ``We will most likely never realize the full importance of painting the Tower,\\ |
12 that it is the essential element in the conservation of metal works and the\\ |
12 that it is the essential element in the conservation of metal works and the\\ |
13 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
13 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
42 does neither support introduction rules involving arbitrary monotonic |
42 does neither support introduction rules involving arbitrary monotonic |
43 operators, nor does it prove case analysis rules (also called inversion rules). |
43 operators, nor does it prove case analysis rules (also called inversion rules). |
44 Moreover, it only proves a weaker form of the induction principle for inductive |
44 Moreover, it only proves a weaker form of the induction principle for inductive |
45 predicates. But it illustrates the implementation pf a typical package in |
45 predicates. But it illustrates the implementation pf a typical package in |
46 Isabelle. |
46 Isabelle. |
47 *} |
47 \<close> |
48 |
48 |
49 end |
49 end |