--- a/src/Pure/Syntax/ROOT.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/ROOT.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/ROOT.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
This file builds the syntax module.
*)
--- a/src/Pure/Syntax/ast.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/ast.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/ast.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Abstract syntax trees, translation rules, matching and normalization of asts.
*)
--- a/src/Pure/Syntax/lexicon.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/lexicon.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Lexer for the inner Isabelle syntax (terms and types).
*)
--- a/src/Pure/Syntax/mixfix.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/mixfix.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Mixfix declarations, infixes, binders. Also parts of the Pure syntax.
*)
--- a/src/Pure/Syntax/parser.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/parser.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/parser.ML
ID: $Id$
Author: Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Isabelle's main parser (used for terms and types).
*)
--- a/src/Pure/Syntax/printer.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/printer.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Pretty printing of asts, terms, types and print (ast) translation.
*)
--- a/src/Pure/Syntax/syn_ext.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/syn_ext.ML
ID: $Id$
Author: Markus Wenzel and Carsten Clasohm, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Syntax extension (internal interface).
*)
--- a/src/Pure/Syntax/syn_trans.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/syn_trans.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Syntax translation functions.
*)
--- a/src/Pure/Syntax/syntax.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/syntax.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Root of Isabelle's syntax module.
*)
--- a/src/Pure/Syntax/token_trans.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/token_trans.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/token_trans.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Token translations for xterm output.
*)
--- a/src/Pure/Syntax/type_ext.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/Syntax/type_ext.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/Syntax/type_ext.ML
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Utilities for input and output of types. Also the concrete syntax of
types, which is required to bootstrap Pure.
--- a/src/Pure/sign.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/sign.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/sign.ML
ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The abstract type "sg" of signatures.
*)
--- a/src/Pure/theory.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/theory.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/theory.ML
ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
- Copyright 1996 University of Cambridge
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The abstract type "theory" of theories.
*)
--- a/src/Pure/theory_data.ML Wed Jan 16 23:18:20 2002 +0100
+++ b/src/Pure/theory_data.ML Wed Jan 16 23:19:34 2002 +0100
@@ -1,6 +1,7 @@
(* Title: Pure/theory_data.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Type-safe interface for theory data.
*)