equal
deleted
inserted
replaced
1 theory Local_Theory |
1 theory Local_Theory |
2 imports Base |
2 imports Base |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Local theory specifications *} |
5 chapter {* Local theory specifications \label{ch:local-theory} *} |
6 |
6 |
7 text {* |
7 text {* |
8 A \emph{local theory} combines aspects of both theory and proof |
8 A \emph{local theory} combines aspects of both theory and proof |
9 context (cf.\ \secref{sec:context}), such that definitional |
9 context (cf.\ \secref{sec:context}), such that definitional |
10 specifications may be given relatively to parameters and |
10 specifications may be given relatively to parameters and |