src/HOL/Prolog/Type.thy
changeset 13208 965f95a3abd9
parent 12338 de0f4a63baa5
child 14981 e73f8140af78
--- a/src/HOL/Prolog/Type.thy	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Type.thy	Tue Jun 11 16:43:17 2002 +0200
@@ -1,4 +1,10 @@
-(* type inference *)
+(*  Title:    HOL/Prolog/Type.thy
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+
+type inference 
+*)
 
 Type = Func +