--- a/src/Pure/General/ROOT.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/ROOT.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/ROOT.ML
- ID: $Id$
Library of general tools.
*)
--- a/src/Pure/General/alist.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/alist.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/alist.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Association lists -- lists of (key, value) pairs.
--- a/src/Pure/General/balanced_tree.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/balanced_tree.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/balanced_tree.ML
- ID: $Id$
Author: Lawrence C Paulson and Makarius
Balanced binary trees.
--- a/src/Pure/General/basics.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/basics.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/basics.ML
- ID: $Id$
Author: Florian Haftmann and Makarius, TU Muenchen
Fundamental concepts.
--- a/src/Pure/General/file.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/file.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/file.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
File system operations.
--- a/src/Pure/General/graph.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/graph.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/graph.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Directed graphs.
--- a/src/Pure/General/heap.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/heap.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,6 +1,5 @@
(* Title: Pure/General/heap.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
+ Author: Lawrence C Paulson and Markus Wenzel
Heaps over linearly ordered types. See also Chris Okasaki: "Purely
Functional Data Structures" (Chapter 3), Cambridge University Press,
--- a/src/Pure/General/integer.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/integer.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/integer.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Unbounded integers.
--- a/src/Pure/General/ord_list.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/ord_list.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/ord_list.ML
- ID: $Id$
Author: Makarius
Ordered lists without duplicates -- a light-weight representation of
--- a/src/Pure/General/output.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/output.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/output.ML
- ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
Output channels and timing messages.
--- a/src/Pure/General/path.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/path.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/path.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Abstract algebra of file paths (external encoding in Unix style).
--- a/src/Pure/General/pretty.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/pretty.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/pretty.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Munich
--- a/src/Pure/General/print_mode.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/print_mode.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/print_mode.ML
- ID: $Id$
Author: Makarius
Generic print mode as thread-local value derived from global template;
--- a/src/Pure/General/properties.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/properties.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/properties.ML
- ID: $Id$
Author: Makarius
Property lists.
--- a/src/Pure/General/queue.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/queue.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/queue.ML
- ID: $Id$
Author: Makarius
Efficient queues.
--- a/src/Pure/General/scan.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/scan.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/scan.ML
- ID: $Id$
Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
Generic scanners (for potentially infinite input).
--- a/src/Pure/General/secure.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/secure.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/secure.ML
- ID: $Id$
Author: Makarius
Secure critical operations.
--- a/src/Pure/General/seq.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/seq.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/seq.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Munich
--- a/src/Pure/General/source.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/source.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/source.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Coalgebraic data sources -- efficient purely functional input streams.
--- a/src/Pure/General/stack.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/stack.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/stack.ML
- ID: $Id$
Author: Makarius
Non-empty stacks.
--- a/src/Pure/General/symbol.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/symbol.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/symbol.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generalized characters with infinitely many named symbols.
--- a/src/Pure/General/symbol_pos.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/symbol_pos.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/symbol_pos.ML
- ID: $Id$
Author: Makarius
Symbols with explicit position information.
--- a/src/Pure/General/table.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/table.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/table.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Generic tables. Efficient purely functional implementation using
--- a/src/Pure/General/url.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/url.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/url.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Basic URLs, see RFC 1738 and RFC 2396.
--- a/src/Pure/General/xml.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/xml.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/xml.ML
- ID: $Id$
Author: David Aspinall, Stefan Berghofer and Markus Wenzel
Basic support for XML.
--- a/src/Pure/General/yxml.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/yxml.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/yxml.ML
- ID: $Id$
Author: Makarius
Efficient text representation of XML trees using extra characters X
--- a/src/Pure/Isar/antiquote.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/antiquote.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/antiquote.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Text with antiquotations of inner items (terms, types etc.).
--- a/src/Pure/Isar/args.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/args.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/args.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Parsing with implicit value assigment. Concrete argument syntax of
--- a/src/Pure/Isar/auto_bind.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/auto_bind.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/auto_bind.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Automatic bindings of Isar text elements.
--- a/src/Pure/Isar/calculation.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/calculation.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic calculational proofs.
--- a/src/Pure/Isar/context_rules.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/context_rules.ML
- ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
Declarations of intro/elim/dest rules in Pure (see also
--- a/src/Pure/Isar/local_syntax.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/local_syntax.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/local_syntax.ML
- ID: $Id$
Author: Makarius
Local syntax depending on theory syntax.
--- a/src/Pure/Isar/net_rules.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/net_rules.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/net_rules.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Efficient storage of rules: preserves order, prefers later entries.
--- a/src/Pure/Isar/object_logic.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/object_logic.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Specifics about common object-logics.
--- a/src/Pure/Isar/outer_lex.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/outer_lex.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/outer_lex.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Outer lexical syntax for Isabelle/Isar.
--- a/src/Pure/Isar/overloading.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/overloading.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Overloaded definitions without any discipline.
--- a/src/Pure/Isar/proof_context.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_context.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
The key concept of Isar proof contexts: elevates primitive local
--- a/src/Pure/Isar/proof_display.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_display.ML
- ID: $Id$
Author: Makarius
Printing of theorems, goals, results etc.
--- a/src/Pure/Isar/proof_node.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_node.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_node.ML
- ID: $Id$
Author: Makarius
Proof nodes with linear position and backtracking.
--- a/src/Pure/Isar/rule_insts.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/rule_insts.ML
- ID: $Id$
Author: Makarius
Rule instantiations -- operations within a rule/subgoal context.
--- a/src/Pure/Isar/skip_proof.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/skip_proof.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Skipping proofs -- quick_and_dirty mode.
--- a/src/Pure/Isar/specification.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/specification.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/specification.ML
- ID: $Id$
Author: Makarius
Derived local theory specifications --- with type-inference and
--- a/src/Pure/ML/ml_antiquote.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_antiquote.ML
- ID: $Id$
Author: Makarius
Common ML antiquotations.
--- a/src/Pure/ML/ml_context.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_context.ML
- ID: $Id$
Author: Makarius
ML context and antiquotations.
--- a/src/Pure/ML/ml_lex.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_lex.ML
- ID: $Id$
Author: Makarius
Lexical syntax for SML.
--- a/src/Pure/ML/ml_parse.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_parse.ML
- ID: $Id$
Author: Makarius
Minimal parsing for SML -- fixing integer numerals.
--- a/src/Pure/ML/ml_syntax.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_syntax.ML
- ID: $Id$
Author: Makarius
Basic ML syntax operations.
--- a/src/Pure/ML/ml_thms.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_thms.ML
- ID: $Id$
Author: Makarius
Isar theorem values within ML.
--- a/src/Pure/Proof/proof_syntax.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Proof/proof_syntax.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Function for parsing and printing proof terms.
--- a/src/Pure/ProofGeneral/ROOT.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/ROOT.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/ROOT.ML
- ID: $Id$
Author: David Aspinall
Proof General interface for Isabelle, both the traditional Emacs version,
--- a/src/Pure/ProofGeneral/pgip.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip.ML
- ID: $Id$
Author: David Aspinall
Prover-side PGIP abstraction.
--- a/src/Pure/ProofGeneral/pgip_input.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_input.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: input commands.
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_isabelle.ML
- ID: $Id$
Author: David Aspinall
Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
--- a/src/Pure/ProofGeneral/pgip_markup.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_markup.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: document markup for proof scripts (in progress).
--- a/src/Pure/ProofGeneral/pgip_output.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_output.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: output commands.
--- a/src/Pure/ProofGeneral/pgip_parser.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_parser.ML
- ID: $Id$
Author: David Aspinall and Makarius
Parsing theory sources without execution (via keyword classification).
--- a/src/Pure/ProofGeneral/pgip_tests.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_tests.ML
- ID: $Id$
Author: David Aspinall
A test suite for the PGIP abstraction code (in progress).
--- a/src/Pure/ProofGeneral/pgip_types.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_types.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: types and conversions.
--- a/src/Pure/ProofGeneral/pgml.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgml.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgml.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: PGML
--- a/src/Pure/ProofGeneral/proof_general_keywords.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_keywords.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/proof_general_keywords.ML
- ID: $Id$
Author: Makarius
Dummy session with outer syntax keyword initialization.
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/proof_general_pgip.ML
- ID: $Id$
Author: David Aspinall and Markus Wenzel
Isabelle configuration for Proof General using PGIP protocol.
--- a/src/Pure/Pure.thy Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Pure.thy Wed Jan 21 23:21:44 2009 +0100
@@ -1,6 +1,3 @@
-(* Title: Pure/Pure.thy
- ID: $Id$
-*)
section {* Further content for the Pure theory *}
--- a/src/Pure/Thy/html.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/html.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/html.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
HTML presentation elements.
--- a/src/Pure/Thy/latex.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/latex.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/latex.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
LaTeX presentation elements -- based on outer lexical syntax.
--- a/src/Pure/Thy/present.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/present.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/present.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Theory presentation: HTML, graph files, (PDF)LaTeX documents.
--- a/src/Pure/Thy/term_style.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/term_style.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/term_style.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Styles for terms, to use with the "term_style" and "thm_style"
--- a/src/Pure/Thy/thm_deps.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thm_deps.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Visualize dependencies of theorems.
--- a/src/Pure/Thy/thy_header.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_header.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory headers -- independent of outer syntax.
--- a/src/Pure/Thy/thy_output.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_output.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory document output.
--- a/src/Pure/Tools/xml_syntax.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/xml_syntax.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Input and output of types, terms, and proofs in XML format.
--- a/src/Pure/config.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/config.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/config.ML
- ID: $Id$
Author: Makarius
Configuration options as values within the local context.
--- a/src/Pure/conjunction.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/conjunction.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/conjunction.ML
- ID: $Id$
Author: Makarius
Meta-level conjunction.
--- a/src/Pure/consts.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/consts.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/consts.ML
- ID: $Id$
Author: Makarius
Polymorphic constants: declarations, abbreviations, additional type
--- a/src/Pure/context_position.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/context_position.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/context_position.ML
- ID: $Id$
Author: Makarius
Context position visibility flag.
--- a/src/Pure/conv.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/conv.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/conv.ML
- ID: $Id$
Author: Amine Chaieb and Makarius
Conversions: primitive equality reasoning.
--- a/src/Pure/defs.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/defs.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/defs.ML
- ID: $Id$
Author: Makarius
Global well-formedness checks for constant definitions. Covers plain
--- a/src/Pure/display.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/display.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/display.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/interpretation.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/interpretation.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/interpretation.ML
- ID: $Id$
Author: Florian Haftmann and Makarius
Generic interpretation of theory data.
--- a/src/Pure/net.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/net.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/net.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/old_goals.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/old_goals.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/old_goals.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/sign.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/sign.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/sign.ML
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
Logical signature content: naming conventions, concrete syntax, type
--- a/src/Pure/simplifier.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/simplifier.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/simplifier.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Generic simplifier, suitable for most logics (see also
--- a/src/Pure/subgoal.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/subgoal.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/subgoal.ML
- ID: $Id$
Author: Makarius
Tactical operations depending on local subgoal structure.
--- a/src/Pure/theory.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/theory.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/theory.ML
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
Logical theory content: axioms, definitions, and begin/end wrappers.
--- a/src/Pure/type_infer.ML Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/type_infer.ML Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/type_infer.ML
- ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
Simple type inference.