changeset 44055 | 65cdd08bd7fd |
parent 43994 | 5de4bde3ad41 |
child 44273 | 336752fb25df |
44054:da5fcc0f6c52 | 44055:65cdd08bd7fd |
---|---|
1 theory HOL_Specific |
1 theory HOL_Specific |
2 imports Base Main |
2 imports Base Main "~~/src/HOL/Library/Old_Recdef" |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Isabelle/HOL \label{ch:hol} *} |
5 chapter {* Isabelle/HOL \label{ch:hol} *} |
6 |
6 |
7 section {* Higher-Order Logic *} |
7 section {* Higher-Order Logic *} |