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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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