# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258682584 -3600
# Node ID 7f7080ce7c2b0b66de5bba25eaca8e8fe9644d7f
# Parent  6b423b39cc118819bfa697c8cce55f938f5e1fcc
started something about sorts

diff -r 6b423b39cc11 -r 7f7080ce7c2b ProgTutorial/Essential.thy
--- 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} *}
 
diff -r 6b423b39cc11 -r 7f7080ce7c2b progtutorial.pdf
Binary file progtutorial.pdf has changed