# HG changeset patch
# User oheimb
# Date 1023806597 -7200
# Node ID 965f95a3abd9f0ca3bb821bea21e3e720b1bee18
# Parent  0d07e49dc9a5d2a4385664d29921c143a33b1ffb
added the usual file headers

diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Func.ML
--- a/src/HOL/Prolog/Func.ML	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Func.ML	Tue Jun 11 16:43:17 2002 +0200
@@ -1,3 +1,9 @@
+(* Title:    HOL/Prolog/Func.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
 open Func;
 
 val prog_Func = prog_HOHH @ [eval];
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Func.thy	Tue Jun 11 16:43:17 2002 +0200
@@ -1,4 +1,10 @@
-(* untyped functional language, with call by value semantics *)
+(*  Title:    HOL/Prolog/Func.thy
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+
+untyped functional language, with call by value semantics 
+*)
 
 Func = HOHH +
 
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/HOHH.ML
--- a/src/HOL/Prolog/HOHH.ML	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/HOHH.ML	Tue Jun 11 16:43:17 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:    HOL/Prolog/HOHH.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
 open HOHH;
 
 exception not_HOHH;
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Tue Jun 11 16:43:17 2002 +0200
@@ -1,4 +1,10 @@
-(* higher-order hereditary Harrop formulas *)
+(*  Title:    HOL/Prolog/HOHH.thy
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+
+higher-order hereditary Harrop formulas 
+*)
 
 HOHH = HOL +
 
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/ROOT.ML
--- a/src/HOL/Prolog/ROOT.ML	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/ROOT.ML	Tue Jun 11 16:43:17 2002 +0200
@@ -1,2 +1,8 @@
+(*  Title:    HOL/Prolog/ROOT.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
 use_thy"Test";
 use_thy"Type";
\ No newline at end of file
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Test.ML
--- a/src/HOL/Prolog/Test.ML	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Test.ML	Tue Jun 11 16:43:17 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:    HOL/Prolog/Test.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
 open Test;
 
 val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Test.thy	Tue Jun 11 16:43:17 2002 +0200
@@ -1,4 +1,10 @@
-(* basic examples *)
+(*  Title:    HOL/Prolog/Test.thy
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+
+basic examples 
+*)
 
 Test = HOHH +
 
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Type.ML
--- a/src/HOL/Prolog/Type.ML	Tue Jun 11 12:35:33 2002 +0200
+++ b/src/HOL/Prolog/Type.ML	Tue Jun 11 16:43:17 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:    HOL/Prolog/Type.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+    License:  GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
 val prog_Type = prog_Func @ [good_typeof,common_typeof];
 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
 val p = ptac prog_Type 1;
diff -r 0d07e49dc9a5 -r 965f95a3abd9 src/HOL/Prolog/Type.thy
--- 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 +