ProgTutorial/Essential.thy
changeset 398 7f7080ce7c2b
parent 396 a2e49e0771b3
child 399 d7d55a5030b5
--- 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} *}