equal
deleted
inserted
replaced
1 theory Ind_Intro |
1 theory Ind_Intro |
2 imports Main |
2 imports "../Base" |
3 begin |
3 begin |
|
4 |
|
5 (*<*) |
|
6 setup{* |
|
7 open_file_with_prelude |
|
8 "Ind_Package_Code.thy" |
|
9 ["theory Ind_Package", "imports Main", "begin"] |
|
10 *} |
|
11 (*>*) |
4 |
12 |
5 chapter {* How to Write a Definitional Package\label{chp:package} *} |
13 chapter {* How to Write a Definitional Package\label{chp:package} *} |
6 |
14 |
7 text {* |
15 text {* |
8 HOL is based on just a few primitive constants, like equality and |
16 HOL is based on just a few primitive constants, like equality and |