--- 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];
--- 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 +
--- 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;
--- 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 +
--- 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
--- 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];
--- 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 +
--- 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;
--- 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 +