GPLed;

--- a/src/Pure/Isar/ROOT.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/ROOT.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
 *)

--- a/src/Pure/Isar/attrib.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/attrib.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Symbolic theorem attributes.
 *)

--- a/src/Pure/Isar/auto_bind.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/auto_bind.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Automatic term bindings -- logic specific patterns.
 

--- a/src/Pure/Isar/calculation.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/calculation.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Support for calculational proofs.
 *)

--- a/src/Pure/Isar/comment.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/comment.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/comment.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Formal comments.
 *)

--- a/src/Pure/Isar/isar.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/isar.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/isar.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Isabelle/Isar main interface.
 *)

--- a/src/Pure/Isar/isar_cmd.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Non-logical toplevel commands.
 *)

--- a/src/Pure/Isar/isar_syn.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/isar_syn.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Isar/Pure outer syntax.
 *)

--- a/src/Pure/Isar/local_defs.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/local_defs.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/local_defs.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Local definitions.
 *)

--- a/src/Pure/Isar/method.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/method.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proof methods.
 *)

--- a/src/Pure/Isar/net_rules.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/net_rules.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/net_rules.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Efficient storage of rules: preserves order, prefers later entries.
 *)

--- a/src/Pure/Isar/obtain.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/obtain.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/obtain.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 The 'obtain' language element -- generalized existence at the level of
 proof texts.

--- a/src/Pure/Isar/outer_lex.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/outer_lex.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Outer lexical syntax for Isabelle/Isar.
 *)

--- a/src/Pure/Isar/outer_parse.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/outer_parse.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Generic parsers for Isabelle/Isar outer syntax.
 *)

--- a/src/Pure/Isar/outer_syntax.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/outer_syntax.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 The global Isabelle/Isar outer syntax.
 *)

--- a/src/Pure/Isar/proof.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/proof.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proof states and methods.
 *)

--- a/src/Pure/Isar/proof_context.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/proof_context.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proof context information.
 *)

--- a/src/Pure/Isar/proof_data.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/proof_data.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/proof_data.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Type-safe interface for proof context data.
 *)

--- a/src/Pure/Isar/proof_history.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/proof_history.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/proof_history.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Histories of proof states, with undo / redo and prev / back.
 *)

--- a/src/Pure/Isar/rule_cases.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/rule_cases.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Manage local contexts of rules.
 *)

--- a/src/Pure/Isar/session.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/session.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/session.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Session management -- maintain state of logic images.
 *)

--- a/src/Pure/Isar/skip_proof.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/skip_proof.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Skipping proofs -- quick_and_dirty mode.
 *)

--- a/src/Pure/Isar/toplevel.ML	Fri May 05 22:02:46 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri May 05 22:09:41 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Isar/toplevel.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 The Isabelle/Isar toplevel.
 *)