equal
deleted
inserted
replaced
1113 Isabelle/Pure. So the @{command typedef} command was described as |
1113 Isabelle/Pure. So the @{command typedef} command was described as |
1114 ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some |
1114 ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some |
1115 local checks of the given type and its representing set. |
1115 local checks of the given type and its representing set. |
1116 |
1116 |
1117 Recent clarification of overloading in the HOL logic proper @{cite |
1117 Recent clarification of overloading in the HOL logic proper @{cite |
1118 "Kuncar-Popescu:2015"} demonstrate how the dissimilar concepts of constant |
1118 "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant |
1119 definitions versus type definitions may be understood uniformly. This |
1119 definitions versus type definitions may be understood uniformly. This |
1120 requires an interpretation of Isabelle/HOL that substantially reforms the |
1120 requires an interpretation of Isabelle/HOL that substantially reforms the |
1121 set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic |
1121 set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic |
1122 view on polymorphism and interpreting only ground types in the |
1122 view on polymorphism and interpreting only ground types in the |
1123 set-theoretic sense of HOL88. Moreover, type-constructors may be |
1123 set-theoretic sense of HOL88. Moreover, type-constructors may be |