equal
deleted
inserted
replaced
1 Isabelle is a generic system for |
1 Isabelle is a generic system for |
2 implementing logical formalisms, and Isabelle/HOL is the specialisation |
2 implementing logical formalisms, and Isabelle/HOL is the specialization |
3 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
3 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
4 HOL step by step following the equation |
4 HOL step by step following the equation |
5 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
5 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
6 We assume that the reader is used to logical and set-theoretic notation |
6 We assume that the reader is used to logical and set-theoretic notation |
7 and is familiar with the basic concepts of functional programming. |
7 and is familiar with the basic concepts of functional programming. |