--- a/ProgTutorial/Essential.thy Thu Nov 19 20:23:15 2009 +0100
+++ b/ProgTutorial/Essential.thy Fri Nov 20 03:03:04 2009 +0100
@@ -5,7 +5,7 @@
(*<*)
setup{*
open_file_with_prelude
- "Esseantial_Code.thy"
+ "Essential_Code.thy"
["theory General", "imports Base FirstSteps", "begin"]
*}
(*>*)
@@ -1110,6 +1110,25 @@
section {* Sorts (TBD) *}
+text {*
+ Free and schematic variables may be annotated with sorts. Sorts are lists
+ of strings, whereby each string stands for a class. Sorts classify types.
+
+*}
+
+
+ML {* Sign.classes_of @{theory} *}
+
+text {*
+ \begin{readmore}
+ Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
+
+ @{ML_file "Pure/sign.ML"}
+ @{ML_file "Pure/sorts.ML"}
+ @{ML_file "Pure/axclass.ML"}
+ \end{readmore}
+*}
+
section {* Type-Checking\label{sec:typechecking} *}