added the usual file headers
authoroheimb
Tue Jun 11 16:43:17 2002 +0200 (2002-06-11)
changeset 13208965f95a3abd9
parent 13207 0d07e49dc9a5
child 13209 e62a6bd3f085
added the usual file headers
src/HOL/Prolog/Func.ML
src/HOL/Prolog/Func.thy
src/HOL/Prolog/HOHH.ML
src/HOL/Prolog/HOHH.thy
src/HOL/Prolog/ROOT.ML
src/HOL/Prolog/Test.ML
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.ML
src/HOL/Prolog/Type.thy
     1.1 --- a/src/HOL/Prolog/Func.ML	Tue Jun 11 12:35:33 2002 +0200
     1.2 +++ b/src/HOL/Prolog/Func.ML	Tue Jun 11 16:43:17 2002 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(* Title:    HOL/Prolog/Func.ML
     1.5 +    ID:       $Id$
     1.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +*)
     1.9 +
    1.10  open Func;
    1.11  
    1.12  val prog_Func = prog_HOHH @ [eval];
     2.1 --- a/src/HOL/Prolog/Func.thy	Tue Jun 11 12:35:33 2002 +0200
     2.2 +++ b/src/HOL/Prolog/Func.thy	Tue Jun 11 16:43:17 2002 +0200
     2.3 @@ -1,4 +1,10 @@
     2.4 -(* untyped functional language, with call by value semantics *)
     2.5 +(*  Title:    HOL/Prolog/Func.thy
     2.6 +    ID:       $Id$
     2.7 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     2.8 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     2.9 +
    2.10 +untyped functional language, with call by value semantics 
    2.11 +*)
    2.12  
    2.13  Func = HOHH +
    2.14  
     3.1 --- a/src/HOL/Prolog/HOHH.ML	Tue Jun 11 12:35:33 2002 +0200
     3.2 +++ b/src/HOL/Prolog/HOHH.ML	Tue Jun 11 16:43:17 2002 +0200
     3.3 @@ -1,3 +1,9 @@
     3.4 +(*  Title:    HOL/Prolog/HOHH.ML
     3.5 +    ID:       $Id$
     3.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     3.7 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     3.8 +*)
     3.9 +
    3.10  open HOHH;
    3.11  
    3.12  exception not_HOHH;
     4.1 --- a/src/HOL/Prolog/HOHH.thy	Tue Jun 11 12:35:33 2002 +0200
     4.2 +++ b/src/HOL/Prolog/HOHH.thy	Tue Jun 11 16:43:17 2002 +0200
     4.3 @@ -1,4 +1,10 @@
     4.4 -(* higher-order hereditary Harrop formulas *)
     4.5 +(*  Title:    HOL/Prolog/HOHH.thy
     4.6 +    ID:       $Id$
     4.7 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4.8 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     4.9 +
    4.10 +higher-order hereditary Harrop formulas 
    4.11 +*)
    4.12  
    4.13  HOHH = HOL +
    4.14  
     5.1 --- a/src/HOL/Prolog/ROOT.ML	Tue Jun 11 12:35:33 2002 +0200
     5.2 +++ b/src/HOL/Prolog/ROOT.ML	Tue Jun 11 16:43:17 2002 +0200
     5.3 @@ -1,2 +1,8 @@
     5.4 +(*  Title:    HOL/Prolog/ROOT.ML
     5.5 +    ID:       $Id$
     5.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     5.7 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     5.8 +*)
     5.9 +
    5.10  use_thy"Test";
    5.11  use_thy"Type";
    5.12 \ No newline at end of file
     6.1 --- a/src/HOL/Prolog/Test.ML	Tue Jun 11 12:35:33 2002 +0200
     6.2 +++ b/src/HOL/Prolog/Test.ML	Tue Jun 11 16:43:17 2002 +0200
     6.3 @@ -1,3 +1,9 @@
     6.4 +(*  Title:    HOL/Prolog/Test.ML
     6.5 +    ID:       $Id$
     6.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     6.7 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     6.8 +*)
     6.9 +
    6.10  open Test;
    6.11  
    6.12  val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
     7.1 --- a/src/HOL/Prolog/Test.thy	Tue Jun 11 12:35:33 2002 +0200
     7.2 +++ b/src/HOL/Prolog/Test.thy	Tue Jun 11 16:43:17 2002 +0200
     7.3 @@ -1,4 +1,10 @@
     7.4 -(* basic examples *)
     7.5 +(*  Title:    HOL/Prolog/Test.thy
     7.6 +    ID:       $Id$
     7.7 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     7.8 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     7.9 +
    7.10 +basic examples 
    7.11 +*)
    7.12  
    7.13  Test = HOHH +
    7.14  
     8.1 --- a/src/HOL/Prolog/Type.ML	Tue Jun 11 12:35:33 2002 +0200
     8.2 +++ b/src/HOL/Prolog/Type.ML	Tue Jun 11 16:43:17 2002 +0200
     8.3 @@ -1,3 +1,9 @@
     8.4 +(*  Title:    HOL/Prolog/Type.ML
     8.5 +    ID:       $Id$
     8.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     8.7 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     8.8 +*)
     8.9 +
    8.10  val prog_Type = prog_Func @ [good_typeof,common_typeof];
    8.11  fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
    8.12  val p = ptac prog_Type 1;
     9.1 --- a/src/HOL/Prolog/Type.thy	Tue Jun 11 12:35:33 2002 +0200
     9.2 +++ b/src/HOL/Prolog/Type.thy	Tue Jun 11 16:43:17 2002 +0200
     9.3 @@ -1,4 +1,10 @@
     9.4 -(* type inference *)
     9.5 +(*  Title:    HOL/Prolog/Type.thy
     9.6 +    ID:       $Id$
     9.7 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     9.8 +    License:  GPL (GNU GENERAL PUBLIC LICENSE)
     9.9 +
    9.10 +type inference 
    9.11 +*)
    9.12  
    9.13  Type = Func +
    9.14