equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 (*<*) |
5 (*<*) |
6 setup{* |
6 setup{* |
7 open_file_with_prelude |
7 open_file_with_prelude |
8 "Esseantial_Code.thy" |
8 "Essential_Code.thy" |
9 ["theory General", "imports Base FirstSteps", "begin"] |
9 ["theory General", "imports Base FirstSteps", "begin"] |
10 *} |
10 *} |
11 (*>*) |
11 (*>*) |
12 |
12 |
13 |
13 |
1108 \end{readmore} |
1108 \end{readmore} |
1109 *} |
1109 *} |
1110 |
1110 |
1111 section {* Sorts (TBD) *} |
1111 section {* Sorts (TBD) *} |
1112 |
1112 |
|
1113 text {* |
|
1114 Free and schematic variables may be annotated with sorts. Sorts are lists |
|
1115 of strings, whereby each string stands for a class. Sorts classify types. |
|
1116 |
|
1117 *} |
|
1118 |
|
1119 |
|
1120 ML {* Sign.classes_of @{theory} *} |
|
1121 |
|
1122 text {* |
|
1123 \begin{readmore} |
|
1124 Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}. |
|
1125 |
|
1126 @{ML_file "Pure/sign.ML"} |
|
1127 @{ML_file "Pure/sorts.ML"} |
|
1128 @{ML_file "Pure/axclass.ML"} |
|
1129 \end{readmore} |
|
1130 *} |
|
1131 |
1113 |
1132 |
1114 section {* Type-Checking\label{sec:typechecking} *} |
1133 section {* Type-Checking\label{sec:typechecking} *} |
1115 |
1134 |
1116 text {* |
1135 text {* |
1117 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1136 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |