--- a/src/HOL/Tools/induct_method.ML Sat Jul 01 19:54:00 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML Sat Jul 01 19:55:22 2000 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/induct_method.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Proof by cases and induction on types and sets.
*)
--- a/src/HOL/Tools/numeral_syntax.ML Sat Jul 01 19:54:00 2000 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Sat Jul 01 19:55:22 2000 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/numeral_syntax.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Concrete syntax for generic numerals. Assumes consts and syntax of
theory HOL/Numeral.
--- a/src/HOL/Tools/record_package.ML Sat Jul 01 19:54:00 2000 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Jul 01 19:55:22 2000 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/record_package.ML
ID: $Id$
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Extensible records with structural subtyping in HOL.
*)
--- a/src/HOL/Tools/typedef_package.ML Sat Jul 01 19:54:00 2000 +0200
+++ b/src/HOL/Tools/typedef_package.ML Sat Jul 01 19:55:22 2000 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/typedef_package.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Gordon/HOL-style type definitions.
*)