--- a/src/HOLCF/adm.ML Fri Aug 31 18:46:48 2001 +0200
+++ b/src/HOLCF/adm.ML Fri Aug 31 22:44:44 2001 +0200
@@ -1,6 +1,7 @@
(* Title: HOLCF/adm.ML
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Admissibility tactic.
--- a/src/Pure/proofterm.ML Fri Aug 31 18:46:48 2001 +0200
+++ b/src/Pure/proofterm.ML Fri Aug 31 22:44:44 2001 +0200
@@ -1,9 +1,9 @@
(* Title: Pure/proofterm.ML
ID: $Id$
- Author: Stefan Berghofer
- Copyright 2000 TU Muenchen
+ Author: Stefan Berghofer, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-LF style proof terms
+LF style proof terms.
*)
infix 8 % %% %%%;