equal
deleted
inserted
replaced
1 theory HOL_Specific |
1 theory HOL_Specific |
2 imports Base Main "~~/src/HOL/Library/Old_Recdef" "~~/src/Tools/Adhoc_Overloading" |
2 imports Base "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Old_Recdef" |
|
3 "~~/src/Tools/Adhoc_Overloading" |
3 begin |
4 begin |
4 |
5 |
5 chapter {* Higher-Order Logic *} |
6 chapter {* Higher-Order Logic *} |
6 |
7 |
7 text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic |
8 text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic |