1.1 --- a/src/Pure/General/ROOT.ML	Wed Jan 21 22:26:49 2009 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Wed Jan 21 23:21:44 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/General/ROOT.ML
     1.5 -    ID:         $Id$
     1.6  
     1.7  Library of general tools.
     1.8  *)

     2.1 --- a/src/Pure/General/alist.ML	Wed Jan 21 22:26:49 2009 +0100
     2.2 +++ b/src/Pure/General/alist.ML	Wed Jan 21 23:21:44 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      Pure/General/alist.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Florian Haftmann, TU Muenchen
     2.7  
     2.8  Association lists -- lists of (key, value) pairs.

     3.1 --- a/src/Pure/General/balanced_tree.ML	Wed Jan 21 22:26:49 2009 +0100
     3.2 +++ b/src/Pure/General/balanced_tree.ML	Wed Jan 21 23:21:44 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      Pure/General/balanced_tree.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Lawrence C Paulson and Makarius
     3.7  
     3.8  Balanced binary trees.

     4.1 --- a/src/Pure/General/basics.ML	Wed Jan 21 22:26:49 2009 +0100
     4.2 +++ b/src/Pure/General/basics.ML	Wed Jan 21 23:21:44 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      Pure/General/basics.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Florian Haftmann and Makarius, TU Muenchen
     4.7  
     4.8  Fundamental concepts.

     5.1 --- a/src/Pure/General/file.ML	Wed Jan 21 22:26:49 2009 +0100
     5.2 +++ b/src/Pure/General/file.ML	Wed Jan 21 23:21:44 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      Pure/General/file.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7  
     5.8  File system operations.

     6.1 --- a/src/Pure/General/graph.ML	Wed Jan 21 22:26:49 2009 +0100
     6.2 +++ b/src/Pure/General/graph.ML	Wed Jan 21 23:21:44 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      Pure/General/graph.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     6.7  
     6.8  Directed graphs.

     7.1 --- a/src/Pure/General/heap.ML	Wed Jan 21 22:26:49 2009 +0100
     7.2 +++ b/src/Pure/General/heap.ML	Wed Jan 21 23:21:44 2009 +0100
     7.3 @@ -1,6 +1,5 @@
     7.4  (*  Title:      Pure/General/heap.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Markus Wenzel, TU Muenchen
     7.7 +    Author:     Lawrence C Paulson and Markus Wenzel
     7.8  
     7.9  Heaps over linearly ordered types.  See also Chris Okasaki: "Purely
    7.10  Functional Data Structures" (Chapter 3), Cambridge University Press,

     8.1 --- a/src/Pure/General/integer.ML	Wed Jan 21 22:26:49 2009 +0100
     8.2 +++ b/src/Pure/General/integer.ML	Wed Jan 21 23:21:44 2009 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      Pure/General/integer.ML
     8.5 -    ID:         $Id$
     8.6      Author:     Florian Haftmann, TU Muenchen
     8.7  
     8.8  Unbounded integers.

     9.1 --- a/src/Pure/General/ord_list.ML	Wed Jan 21 22:26:49 2009 +0100
     9.2 +++ b/src/Pure/General/ord_list.ML	Wed Jan 21 23:21:44 2009 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      Pure/General/ord_list.ML
     9.5 -    ID:         $Id$
     9.6      Author:     Makarius
     9.7  
     9.8  Ordered lists without duplicates -- a light-weight representation of

    10.1 --- a/src/Pure/General/output.ML	Wed Jan 21 22:26:49 2009 +0100
    10.2 +++ b/src/Pure/General/output.ML	Wed Jan 21 23:21:44 2009 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      Pure/General/output.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
    10.7  
    10.8  Output channels and timing messages.

    11.1 --- a/src/Pure/General/path.ML	Wed Jan 21 22:26:49 2009 +0100
    11.2 +++ b/src/Pure/General/path.ML	Wed Jan 21 23:21:44 2009 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      Pure/General/path.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Markus Wenzel, TU Muenchen
    11.7  
    11.8  Abstract algebra of file paths (external encoding in Unix style).

    12.1 --- a/src/Pure/General/pretty.ML	Wed Jan 21 22:26:49 2009 +0100
    12.2 +++ b/src/Pure/General/pretty.ML	Wed Jan 21 23:21:44 2009 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      Pure/General/pretty.ML
    12.5 -    ID:         $Id$
    12.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7      Author:     Markus Wenzel, TU Munich
    12.8  

    13.1 --- a/src/Pure/General/print_mode.ML	Wed Jan 21 22:26:49 2009 +0100
    13.2 +++ b/src/Pure/General/print_mode.ML	Wed Jan 21 23:21:44 2009 +0100
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      Pure/General/print_mode.ML
    13.5 -    ID:         $Id$
    13.6      Author:     Makarius
    13.7  
    13.8  Generic print mode as thread-local value derived from global template;

    14.1 --- a/src/Pure/General/properties.ML	Wed Jan 21 22:26:49 2009 +0100
    14.2 +++ b/src/Pure/General/properties.ML	Wed Jan 21 23:21:44 2009 +0100
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      Pure/General/properties.ML
    14.5 -    ID:         $Id$
    14.6      Author:     Makarius
    14.7  
    14.8  Property lists.

    15.1 --- a/src/Pure/General/queue.ML	Wed Jan 21 22:26:49 2009 +0100
    15.2 +++ b/src/Pure/General/queue.ML	Wed Jan 21 23:21:44 2009 +0100
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      Pure/General/queue.ML
    15.5 -    ID:         $Id$
    15.6      Author:     Makarius
    15.7  
    15.8  Efficient queues.

    16.1 --- a/src/Pure/General/scan.ML	Wed Jan 21 22:26:49 2009 +0100
    16.2 +++ b/src/Pure/General/scan.ML	Wed Jan 21 23:21:44 2009 +0100
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      Pure/General/scan.ML
    16.5 -    ID:         $Id$
    16.6      Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
    16.7  
    16.8  Generic scanners (for potentially infinite input).

    17.1 --- a/src/Pure/General/secure.ML	Wed Jan 21 22:26:49 2009 +0100
    17.2 +++ b/src/Pure/General/secure.ML	Wed Jan 21 23:21:44 2009 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      Pure/General/secure.ML
    17.5 -    ID:         $Id$
    17.6      Author:     Makarius
    17.7  
    17.8  Secure critical operations.

    18.1 --- a/src/Pure/General/seq.ML	Wed Jan 21 22:26:49 2009 +0100
    18.2 +++ b/src/Pure/General/seq.ML	Wed Jan 21 23:21:44 2009 +0100
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      Pure/General/seq.ML
    18.5 -    ID:         $Id$
    18.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7      Author:     Markus Wenzel, TU Munich
    18.8  

    19.1 --- a/src/Pure/General/source.ML	Wed Jan 21 22:26:49 2009 +0100
    19.2 +++ b/src/Pure/General/source.ML	Wed Jan 21 23:21:44 2009 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      Pure/General/source.ML
    19.5 -    ID:         $Id$
    19.6      Author:     Markus Wenzel, TU Muenchen
    19.7  
    19.8  Coalgebraic data sources -- efficient purely functional input streams.

    20.1 --- a/src/Pure/General/stack.ML	Wed Jan 21 22:26:49 2009 +0100
    20.2 +++ b/src/Pure/General/stack.ML	Wed Jan 21 23:21:44 2009 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      Pure/General/stack.ML
    20.5 -    ID:         $Id$
    20.6      Author:     Makarius
    20.7  
    20.8  Non-empty stacks.

    21.1 --- a/src/Pure/General/symbol.ML	Wed Jan 21 22:26:49 2009 +0100
    21.2 +++ b/src/Pure/General/symbol.ML	Wed Jan 21 23:21:44 2009 +0100
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      Pure/General/symbol.ML
    21.5 -    ID:         $Id$
    21.6      Author:     Markus Wenzel, TU Muenchen
    21.7  
    21.8  Generalized characters with infinitely many named symbols.

    22.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jan 21 22:26:49 2009 +0100
    22.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jan 21 23:21:44 2009 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      Pure/General/symbol_pos.ML
    22.5 -    ID:         $Id$
    22.6      Author:     Makarius
    22.7  
    22.8  Symbols with explicit position information.

    23.1 --- a/src/Pure/General/table.ML	Wed Jan 21 22:26:49 2009 +0100
    23.2 +++ b/src/Pure/General/table.ML	Wed Jan 21 23:21:44 2009 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      Pure/General/table.ML
    23.5 -    ID:         $Id$
    23.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    23.7  
    23.8  Generic tables.  Efficient purely functional implementation using

    24.1 --- a/src/Pure/General/url.ML	Wed Jan 21 22:26:49 2009 +0100
    24.2 +++ b/src/Pure/General/url.ML	Wed Jan 21 23:21:44 2009 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      Pure/General/url.ML
    24.5 -    ID:         $Id$
    24.6      Author:     Markus Wenzel, TU Muenchen
    24.7  
    24.8  Basic URLs, see RFC 1738 and RFC 2396.

    25.1 --- a/src/Pure/General/xml.ML	Wed Jan 21 22:26:49 2009 +0100
    25.2 +++ b/src/Pure/General/xml.ML	Wed Jan 21 23:21:44 2009 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      Pure/General/xml.ML
    25.5 -    ID:         $Id$
    25.6      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
    25.7  
    25.8  Basic support for XML.

    26.1 --- a/src/Pure/General/yxml.ML	Wed Jan 21 22:26:49 2009 +0100
    26.2 +++ b/src/Pure/General/yxml.ML	Wed Jan 21 23:21:44 2009 +0100
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      Pure/General/yxml.ML
    26.5 -    ID:         $Id$
    26.6      Author:     Makarius
    26.7  
    26.8  Efficient text representation of XML trees using extra characters X

    27.1 --- a/src/Pure/Isar/antiquote.ML	Wed Jan 21 22:26:49 2009 +0100
    27.2 +++ b/src/Pure/Isar/antiquote.ML	Wed Jan 21 23:21:44 2009 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      Pure/Isar/antiquote.ML
    27.5 -    ID:         $Id$
    27.6      Author:     Markus Wenzel, TU Muenchen
    27.7  
    27.8  Text with antiquotations of inner items (terms, types etc.).

    28.1 --- a/src/Pure/Isar/args.ML	Wed Jan 21 22:26:49 2009 +0100
    28.2 +++ b/src/Pure/Isar/args.ML	Wed Jan 21 23:21:44 2009 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      Pure/Isar/args.ML
    28.5 -    ID:         $Id$
    28.6      Author:     Markus Wenzel, TU Muenchen
    28.7  
    28.8  Parsing with implicit value assigment.  Concrete argument syntax of

    29.1 --- a/src/Pure/Isar/auto_bind.ML	Wed Jan 21 22:26:49 2009 +0100
    29.2 +++ b/src/Pure/Isar/auto_bind.ML	Wed Jan 21 23:21:44 2009 +0100
    29.3 @@ -1,5 +1,4 @@
    29.4  (*  Title:      Pure/Isar/auto_bind.ML
    29.5 -    ID:         $Id$
    29.6      Author:     Markus Wenzel, TU Muenchen
    29.7  
    29.8  Automatic bindings of Isar text elements.

    30.1 --- a/src/Pure/Isar/calculation.ML	Wed Jan 21 22:26:49 2009 +0100
    30.2 +++ b/src/Pure/Isar/calculation.ML	Wed Jan 21 23:21:44 2009 +0100
    30.3 @@ -1,5 +1,4 @@
    30.4  (*  Title:      Pure/Isar/calculation.ML
    30.5 -    ID:         $Id$
    30.6      Author:     Markus Wenzel, TU Muenchen
    30.7  
    30.8  Generic calculational proofs.

    31.1 --- a/src/Pure/Isar/context_rules.ML	Wed Jan 21 22:26:49 2009 +0100
    31.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Jan 21 23:21:44 2009 +0100
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      Pure/Isar/context_rules.ML
    31.5 -    ID:         $Id$
    31.6      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    31.7  
    31.8  Declarations of intro/elim/dest rules in Pure (see also

    32.1 --- a/src/Pure/Isar/local_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
    32.2 +++ b/src/Pure/Isar/local_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
    32.3 @@ -1,5 +1,4 @@
    32.4  (*  Title:      Pure/Isar/local_syntax.ML
    32.5 -    ID:         $Id$
    32.6      Author:     Makarius
    32.7  
    32.8  Local syntax depending on theory syntax.

    33.1 --- a/src/Pure/Isar/net_rules.ML	Wed Jan 21 22:26:49 2009 +0100
    33.2 +++ b/src/Pure/Isar/net_rules.ML	Wed Jan 21 23:21:44 2009 +0100
    33.3 @@ -1,5 +1,4 @@
    33.4  (*  Title:      Pure/Isar/net_rules.ML
    33.5 -    ID:         $Id$
    33.6      Author:     Markus Wenzel, TU Muenchen
    33.7  
    33.8  Efficient storage of rules: preserves order, prefers later entries.

    34.1 --- a/src/Pure/Isar/object_logic.ML	Wed Jan 21 22:26:49 2009 +0100
    34.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Jan 21 23:21:44 2009 +0100
    34.3 @@ -1,5 +1,4 @@
    34.4  (*  Title:      Pure/Isar/object_logic.ML
    34.5 -    ID:         $Id$
    34.6      Author:     Markus Wenzel, TU Muenchen
    34.7  
    34.8  Specifics about common object-logics.

    35.1 --- a/src/Pure/Isar/outer_lex.ML	Wed Jan 21 22:26:49 2009 +0100
    35.2 +++ b/src/Pure/Isar/outer_lex.ML	Wed Jan 21 23:21:44 2009 +0100
    35.3 @@ -1,5 +1,4 @@
    35.4  (*  Title:      Pure/Isar/outer_lex.ML
    35.5 -    ID:         $Id$
    35.6      Author:     Markus Wenzel, TU Muenchen
    35.7  
    35.8  Outer lexical syntax for Isabelle/Isar.

    36.1 --- a/src/Pure/Isar/overloading.ML	Wed Jan 21 22:26:49 2009 +0100
    36.2 +++ b/src/Pure/Isar/overloading.ML	Wed Jan 21 23:21:44 2009 +0100
    36.3 @@ -1,5 +1,4 @@
    36.4  (*  Title:      Pure/Isar/overloading.ML
    36.5 -    ID:         $Id$
    36.6      Author:     Florian Haftmann, TU Muenchen
    36.7  
    36.8  Overloaded definitions without any discipline.

    37.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jan 21 22:26:49 2009 +0100
    37.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jan 21 23:21:44 2009 +0100
    37.3 @@ -1,5 +1,4 @@
    37.4  (*  Title:      Pure/Isar/proof_context.ML
    37.5 -    ID:         $Id$
    37.6      Author:     Markus Wenzel, TU Muenchen
    37.7  
    37.8  The key concept of Isar proof contexts: elevates primitive local

    38.1 --- a/src/Pure/Isar/proof_display.ML	Wed Jan 21 22:26:49 2009 +0100
    38.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Jan 21 23:21:44 2009 +0100
    38.3 @@ -1,5 +1,4 @@
    38.4  (*  Title:      Pure/Isar/proof_display.ML
    38.5 -    ID:         $Id$
    38.6      Author:     Makarius
    38.7  
    38.8  Printing of theorems, goals, results etc.

    39.1 --- a/src/Pure/Isar/proof_node.ML	Wed Jan 21 22:26:49 2009 +0100
    39.2 +++ b/src/Pure/Isar/proof_node.ML	Wed Jan 21 23:21:44 2009 +0100
    39.3 @@ -1,5 +1,4 @@
    39.4  (*  Title:      Pure/Isar/proof_node.ML
    39.5 -    ID:         $Id$
    39.6      Author:     Makarius
    39.7  
    39.8  Proof nodes with linear position and backtracking.

    40.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Jan 21 22:26:49 2009 +0100
    40.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Jan 21 23:21:44 2009 +0100
    40.3 @@ -1,5 +1,4 @@
    40.4  (*  Title:      Pure/Isar/rule_insts.ML
    40.5 -    ID:         $Id$
    40.6      Author:     Makarius
    40.7  
    40.8  Rule instantiations -- operations within a rule/subgoal context.

    41.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Jan 21 22:26:49 2009 +0100
    41.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Jan 21 23:21:44 2009 +0100
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      Pure/Isar/skip_proof.ML
    41.5 -    ID:         $Id$
    41.6      Author:     Markus Wenzel, TU Muenchen
    41.7  
    41.8  Skipping proofs -- quick_and_dirty mode.

    42.1 --- a/src/Pure/Isar/specification.ML	Wed Jan 21 22:26:49 2009 +0100
    42.2 +++ b/src/Pure/Isar/specification.ML	Wed Jan 21 23:21:44 2009 +0100
    42.3 @@ -1,5 +1,4 @@
    42.4  (*  Title:      Pure/Isar/specification.ML
    42.5 -    ID:         $Id$
    42.6      Author:     Makarius
    42.7  
    42.8  Derived local theory specifications --- with type-inference and

    43.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Jan 21 22:26:49 2009 +0100
    43.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Jan 21 23:21:44 2009 +0100
    43.3 @@ -1,5 +1,4 @@
    43.4  (*  Title:      Pure/ML/ml_antiquote.ML
    43.5 -    ID:         $Id$
    43.6      Author:     Makarius
    43.7  
    43.8  Common ML antiquotations.

    44.1 --- a/src/Pure/ML/ml_context.ML	Wed Jan 21 22:26:49 2009 +0100
    44.2 +++ b/src/Pure/ML/ml_context.ML	Wed Jan 21 23:21:44 2009 +0100
    44.3 @@ -1,5 +1,4 @@
    44.4  (*  Title:      Pure/ML/ml_context.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Makarius
    44.7  
    44.8  ML context and antiquotations.

    45.1 --- a/src/Pure/ML/ml_lex.ML	Wed Jan 21 22:26:49 2009 +0100
    45.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Jan 21 23:21:44 2009 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      Pure/ML/ml_lex.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Makarius
    45.7  
    45.8  Lexical syntax for SML.

    46.1 --- a/src/Pure/ML/ml_parse.ML	Wed Jan 21 22:26:49 2009 +0100
    46.2 +++ b/src/Pure/ML/ml_parse.ML	Wed Jan 21 23:21:44 2009 +0100
    46.3 @@ -1,5 +1,4 @@
    46.4  (*  Title:      Pure/ML/ml_parse.ML
    46.5 -    ID:         $Id$
    46.6      Author:     Makarius
    46.7  
    46.8  Minimal parsing for SML -- fixing integer numerals.

    47.1 --- a/src/Pure/ML/ml_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
    47.2 +++ b/src/Pure/ML/ml_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
    47.3 @@ -1,5 +1,4 @@
    47.4  (*  Title:      Pure/ML/ml_syntax.ML
    47.5 -    ID:         $Id$
    47.6      Author:     Makarius
    47.7  
    47.8  Basic ML syntax operations.

    48.1 --- a/src/Pure/ML/ml_thms.ML	Wed Jan 21 22:26:49 2009 +0100
    48.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Jan 21 23:21:44 2009 +0100
    48.3 @@ -1,5 +1,4 @@
    48.4  (*  Title:      Pure/ML/ml_thms.ML
    48.5 -    ID:         $Id$
    48.6      Author:     Makarius
    48.7  
    48.8  Isar theorem values within ML.

    49.1 --- a/src/Pure/Proof/proof_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
    49.2 +++ b/src/Pure/Proof/proof_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
    49.3 @@ -1,5 +1,4 @@
    49.4  (*  Title:      Pure/Proof/proof_syntax.ML
    49.5 -    ID:         $Id$
    49.6      Author:     Stefan Berghofer, TU Muenchen
    49.7  
    49.8  Function for parsing and printing proof terms.

    50.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Wed Jan 21 22:26:49 2009 +0100
    50.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Wed Jan 21 23:21:44 2009 +0100
    50.3 @@ -1,5 +1,4 @@
    50.4  (*  Title:      Pure/ProofGeneral/ROOT.ML
    50.5 -    ID:         $Id$
    50.6      Author:     David Aspinall
    50.7  
    50.8  Proof General interface for Isabelle, both the traditional Emacs version,

    51.1 --- a/src/Pure/ProofGeneral/pgip.ML	Wed Jan 21 22:26:49 2009 +0100
    51.2 +++ b/src/Pure/ProofGeneral/pgip.ML	Wed Jan 21 23:21:44 2009 +0100
    51.3 @@ -1,5 +1,4 @@
    51.4  (*  Title:      Pure/ProofGeneral/pgip.ML
    51.5 -    ID:         $Id$
    51.6      Author:     David Aspinall
    51.7  
    51.8  Prover-side PGIP abstraction.  

    52.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Jan 21 22:26:49 2009 +0100
    52.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed Jan 21 23:21:44 2009 +0100
    52.3 @@ -1,5 +1,4 @@
    52.4  (*  Title:      Pure/ProofGeneral/pgip_input.ML
    52.5 -    ID:         $Id$
    52.6      Author:     David Aspinall
    52.7  
    52.8  PGIP abstraction: input commands.

    53.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Jan 21 22:26:49 2009 +0100
    53.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Jan 21 23:21:44 2009 +0100
    53.3 @@ -1,5 +1,4 @@
    53.4  (*  Title:      Pure/ProofGeneral/pgip_isabelle.ML
    53.5 -    ID:         $Id$
    53.6      Author:     David Aspinall
    53.7  
    53.8  Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.

    54.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML	Wed Jan 21 22:26:49 2009 +0100
    54.2 +++ b/src/Pure/ProofGeneral/pgip_markup.ML	Wed Jan 21 23:21:44 2009 +0100
    54.3 @@ -1,5 +1,4 @@
    54.4  (*  Title:      Pure/ProofGeneral/pgip_markup.ML
    54.5 -    ID:         $Id$
    54.6      Author:     David Aspinall
    54.7  
    54.8  PGIP abstraction: document markup for proof scripts (in progress).

    55.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Wed Jan 21 22:26:49 2009 +0100
    55.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Wed Jan 21 23:21:44 2009 +0100
    55.3 @@ -1,5 +1,4 @@
    55.4  (*  Title:      Pure/ProofGeneral/pgip_output.ML
    55.5 -    ID:         $Id$
    55.6      Author:     David Aspinall
    55.7  
    55.8  PGIP abstraction: output commands.

    56.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jan 21 22:26:49 2009 +0100
    56.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jan 21 23:21:44 2009 +0100
    56.3 @@ -1,5 +1,4 @@
    56.4  (*  Title:      Pure/ProofGeneral/pgip_parser.ML
    56.5 -    ID:         $Id$
    56.6      Author:     David Aspinall and Makarius
    56.7  
    56.8  Parsing theory sources without execution (via keyword classification).

    57.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jan 21 22:26:49 2009 +0100
    57.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jan 21 23:21:44 2009 +0100
    57.3 @@ -1,5 +1,4 @@
    57.4  (*  Title:      Pure/ProofGeneral/pgip_tests.ML
    57.5 -    ID:         $Id$
    57.6      Author:     David Aspinall
    57.7  
    57.8  A test suite for the PGIP abstraction code (in progress).

    58.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Jan 21 22:26:49 2009 +0100
    58.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Jan 21 23:21:44 2009 +0100
    58.3 @@ -1,5 +1,4 @@
    58.4  (*  Title:      Pure/ProofGeneral/pgip_types.ML
    58.5 -    ID:         $Id$
    58.6      Author:     David Aspinall
    58.7  
    58.8  PGIP abstraction: types and conversions.

    59.1 --- a/src/Pure/ProofGeneral/pgml.ML	Wed Jan 21 22:26:49 2009 +0100
    59.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Wed Jan 21 23:21:44 2009 +0100
    59.3 @@ -1,5 +1,4 @@
    59.4  (*  Title:      Pure/ProofGeneral/pgml.ML
    59.5 -    ID:         $Id$
    59.6      Author:     David Aspinall
    59.7  
    59.8  PGIP abstraction: PGML

    60.1 --- a/src/Pure/ProofGeneral/proof_general_keywords.ML	Wed Jan 21 22:26:49 2009 +0100
    60.2 +++ b/src/Pure/ProofGeneral/proof_general_keywords.ML	Wed Jan 21 23:21:44 2009 +0100
    60.3 @@ -1,5 +1,4 @@
    60.4  (*  Title:      Pure/ProofGeneral/proof_general_keywords.ML
    60.5 -    ID:         $Id$
    60.6      Author:     Makarius
    60.7  
    60.8  Dummy session with outer syntax keyword initialization.

    61.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 21 22:26:49 2009 +0100
    61.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 21 23:21:44 2009 +0100
    61.3 @@ -1,5 +1,4 @@
    61.4  (*  Title:      Pure/ProofGeneral/proof_general_pgip.ML
    61.5 -    ID:         $Id$
    61.6      Author:     David Aspinall and Markus Wenzel
    61.7  
    61.8  Isabelle configuration for Proof General using PGIP protocol.

    62.1 --- a/src/Pure/Pure.thy	Wed Jan 21 22:26:49 2009 +0100
    62.2 +++ b/src/Pure/Pure.thy	Wed Jan 21 23:21:44 2009 +0100
    62.3 @@ -1,6 +1,3 @@
    62.4 -(*  Title:      Pure/Pure.thy
    62.5 -    ID:         $Id$
    62.6 -*)
    62.7  
    62.8  section {* Further content for the Pure theory *}
    62.9  

    63.1 --- a/src/Pure/Thy/html.ML	Wed Jan 21 22:26:49 2009 +0100
    63.2 +++ b/src/Pure/Thy/html.ML	Wed Jan 21 23:21:44 2009 +0100
    63.3 @@ -1,5 +1,4 @@
    63.4  (*  Title:      Pure/Thy/html.ML
    63.5 -    ID:         $Id$
    63.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    63.7  
    63.8  HTML presentation elements.

    64.1 --- a/src/Pure/Thy/latex.ML	Wed Jan 21 22:26:49 2009 +0100
    64.2 +++ b/src/Pure/Thy/latex.ML	Wed Jan 21 23:21:44 2009 +0100
    64.3 @@ -1,5 +1,4 @@
    64.4  (*  Title:      Pure/Thy/latex.ML
    64.5 -    ID:         $Id$
    64.6      Author:     Markus Wenzel, TU Muenchen
    64.7  
    64.8  LaTeX presentation elements -- based on outer lexical syntax.

    65.1 --- a/src/Pure/Thy/present.ML	Wed Jan 21 22:26:49 2009 +0100
    65.2 +++ b/src/Pure/Thy/present.ML	Wed Jan 21 23:21:44 2009 +0100
    65.3 @@ -1,5 +1,4 @@
    65.4  (*  Title:      Pure/Thy/present.ML
    65.5 -    ID:         $Id$
    65.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    65.7  
    65.8  Theory presentation: HTML, graph files, (PDF)LaTeX documents.

    66.1 --- a/src/Pure/Thy/term_style.ML	Wed Jan 21 22:26:49 2009 +0100
    66.2 +++ b/src/Pure/Thy/term_style.ML	Wed Jan 21 23:21:44 2009 +0100
    66.3 @@ -1,5 +1,4 @@
    66.4  (*  Title:      Pure/Thy/term_style.ML
    66.5 -    ID:         $Id$
    66.6      Author:     Florian Haftmann, TU Muenchen
    66.7  
    66.8  Styles for terms, to use with the "term_style" and "thm_style"

    67.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Jan 21 22:26:49 2009 +0100
    67.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Jan 21 23:21:44 2009 +0100
    67.3 @@ -1,5 +1,4 @@
    67.4  (*  Title:      Pure/Thy/thm_deps.ML
    67.5 -    ID:         $Id$
    67.6      Author:     Stefan Berghofer, TU Muenchen
    67.7  
    67.8  Visualize dependencies of theorems.

    68.1 --- a/src/Pure/Thy/thy_header.ML	Wed Jan 21 22:26:49 2009 +0100
    68.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Jan 21 23:21:44 2009 +0100
    68.3 @@ -1,5 +1,4 @@
    68.4  (*  Title:      Pure/Thy/thy_header.ML
    68.5 -    ID:         $Id$
    68.6      Author:     Markus Wenzel, TU Muenchen
    68.7  
    68.8  Theory headers -- independent of outer syntax.

    69.1 --- a/src/Pure/Thy/thy_output.ML	Wed Jan 21 22:26:49 2009 +0100
    69.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Jan 21 23:21:44 2009 +0100
    69.3 @@ -1,5 +1,4 @@
    69.4  (*  Title:      Pure/Thy/thy_output.ML
    69.5 -    ID:         $Id$
    69.6      Author:     Markus Wenzel, TU Muenchen
    69.7  
    69.8  Theory document output.

    70.1 --- a/src/Pure/Tools/xml_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
    70.2 +++ b/src/Pure/Tools/xml_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
    70.3 @@ -1,5 +1,4 @@
    70.4  (*  Title:      Pure/Tools/xml_syntax.ML
    70.5 -    ID:         $Id$
    70.6      Author:     Stefan Berghofer, TU Muenchen
    70.7  
    70.8  Input and output of types, terms, and proofs in XML format.

    71.1 --- a/src/Pure/config.ML	Wed Jan 21 22:26:49 2009 +0100
    71.2 +++ b/src/Pure/config.ML	Wed Jan 21 23:21:44 2009 +0100
    71.3 @@ -1,5 +1,4 @@
    71.4  (*  Title:      Pure/config.ML
    71.5 -    ID:         $Id$
    71.6      Author:     Makarius
    71.7  
    71.8  Configuration options as values within the local context.

    72.1 --- a/src/Pure/conjunction.ML	Wed Jan 21 22:26:49 2009 +0100
    72.2 +++ b/src/Pure/conjunction.ML	Wed Jan 21 23:21:44 2009 +0100
    72.3 @@ -1,5 +1,4 @@
    72.4  (*  Title:      Pure/conjunction.ML
    72.5 -    ID:         $Id$
    72.6      Author:     Makarius
    72.7  
    72.8  Meta-level conjunction.

    73.1 --- a/src/Pure/consts.ML	Wed Jan 21 22:26:49 2009 +0100
    73.2 +++ b/src/Pure/consts.ML	Wed Jan 21 23:21:44 2009 +0100
    73.3 @@ -1,5 +1,4 @@
    73.4  (*  Title:      Pure/consts.ML
    73.5 -    ID:         $Id$
    73.6      Author:     Makarius
    73.7  
    73.8  Polymorphic constants: declarations, abbreviations, additional type

    74.1 --- a/src/Pure/context_position.ML	Wed Jan 21 22:26:49 2009 +0100
    74.2 +++ b/src/Pure/context_position.ML	Wed Jan 21 23:21:44 2009 +0100
    74.3 @@ -1,5 +1,4 @@
    74.4  (*  Title:      Pure/context_position.ML
    74.5 -    ID:         $Id$
    74.6      Author:     Makarius
    74.7  
    74.8  Context position visibility flag.

    75.1 --- a/src/Pure/conv.ML	Wed Jan 21 22:26:49 2009 +0100
    75.2 +++ b/src/Pure/conv.ML	Wed Jan 21 23:21:44 2009 +0100
    75.3 @@ -1,5 +1,4 @@
    75.4  (*  Title:      Pure/conv.ML
    75.5 -    ID:         $Id$
    75.6      Author:     Amine Chaieb and Makarius
    75.7  
    75.8  Conversions: primitive equality reasoning.

    76.1 --- a/src/Pure/defs.ML	Wed Jan 21 22:26:49 2009 +0100
    76.2 +++ b/src/Pure/defs.ML	Wed Jan 21 23:21:44 2009 +0100
    76.3 @@ -1,5 +1,4 @@
    76.4  (*  Title:      Pure/defs.ML
    76.5 -    ID:         $Id$
    76.6      Author:     Makarius
    76.7  
    76.8  Global well-formedness checks for constant definitions.  Covers plain

    77.1 --- a/src/Pure/display.ML	Wed Jan 21 22:26:49 2009 +0100
    77.2 +++ b/src/Pure/display.ML	Wed Jan 21 23:21:44 2009 +0100
    77.3 @@ -1,5 +1,4 @@
    77.4  (*  Title:      Pure/display.ML
    77.5 -    ID:         $Id$
    77.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    77.7      Copyright   1993  University of Cambridge
    77.8  

    78.1 --- a/src/Pure/interpretation.ML	Wed Jan 21 22:26:49 2009 +0100
    78.2 +++ b/src/Pure/interpretation.ML	Wed Jan 21 23:21:44 2009 +0100
    78.3 @@ -1,5 +1,4 @@
    78.4  (*  Title:      Pure/interpretation.ML
    78.5 -    ID:         $Id$
    78.6      Author:     Florian Haftmann and Makarius
    78.7  
    78.8  Generic interpretation of theory data.

    79.1 --- a/src/Pure/net.ML	Wed Jan 21 22:26:49 2009 +0100
    79.2 +++ b/src/Pure/net.ML	Wed Jan 21 23:21:44 2009 +0100
    79.3 @@ -1,5 +1,4 @@
    79.4  (*  Title:      Pure/net.ML
    79.5 -    ID:         $Id$
    79.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    79.7      Copyright   1993  University of Cambridge
    79.8  

    80.1 --- a/src/Pure/old_goals.ML	Wed Jan 21 22:26:49 2009 +0100
    80.2 +++ b/src/Pure/old_goals.ML	Wed Jan 21 23:21:44 2009 +0100
    80.3 @@ -1,5 +1,4 @@
    80.4  (*  Title:      Pure/old_goals.ML
    80.5 -    ID:         $Id$
    80.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    80.7      Copyright   1993  University of Cambridge
    80.8  

    81.1 --- a/src/Pure/sign.ML	Wed Jan 21 22:26:49 2009 +0100
    81.2 +++ b/src/Pure/sign.ML	Wed Jan 21 23:21:44 2009 +0100
    81.3 @@ -1,5 +1,4 @@
    81.4  (*  Title:      Pure/sign.ML
    81.5 -    ID:         $Id$
    81.6      Author:     Lawrence C Paulson and Markus Wenzel
    81.7  
    81.8  Logical signature content: naming conventions, concrete syntax, type

    82.1 --- a/src/Pure/simplifier.ML	Wed Jan 21 22:26:49 2009 +0100
    82.2 +++ b/src/Pure/simplifier.ML	Wed Jan 21 23:21:44 2009 +0100
    82.3 @@ -1,5 +1,4 @@
    82.4  (*  Title:      Pure/simplifier.ML
    82.5 -    ID:         $Id$
    82.6      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    82.7  
    82.8  Generic simplifier, suitable for most logics (see also

    83.1 --- a/src/Pure/subgoal.ML	Wed Jan 21 22:26:49 2009 +0100
    83.2 +++ b/src/Pure/subgoal.ML	Wed Jan 21 23:21:44 2009 +0100
    83.3 @@ -1,5 +1,4 @@
    83.4  (*  Title:      Pure/subgoal.ML
    83.5 -    ID:         $Id$
    83.6      Author:     Makarius
    83.7  
    83.8  Tactical operations depending on local subgoal structure.

    84.1 --- a/src/Pure/theory.ML	Wed Jan 21 22:26:49 2009 +0100
    84.2 +++ b/src/Pure/theory.ML	Wed Jan 21 23:21:44 2009 +0100
    84.3 @@ -1,5 +1,4 @@
    84.4  (*  Title:      Pure/theory.ML
    84.5 -    ID:         $Id$
    84.6      Author:     Lawrence C Paulson and Markus Wenzel
    84.7  
    84.8  Logical theory content: axioms, definitions, and begin/end wrappers.

    85.1 --- a/src/Pure/type_infer.ML	Wed Jan 21 22:26:49 2009 +0100
    85.2 +++ b/src/Pure/type_infer.ML	Wed Jan 21 23:21:44 2009 +0100
    85.3 @@ -1,5 +1,4 @@
    85.4  (*  Title:      Pure/type_infer.ML
    85.5 -    ID:         $Id$
    85.6      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    85.7  
    85.8  Simple type inference.