# HG changeset patch # User wenzelm # Date 916237082 -3600 # Node ID caa43943566638f0dc80aac112ddbd011d5501b8 # Parent f9aad8ccd59067b82870d7cbde0d7d76874c9a48 fixed titles; diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/file.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Thy/file.ML +(* Title: Pure/General/file.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/name_space.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/name_space.ML +(* Title: Pure/General/name_space.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/object.ML --- a/src/Pure/General/object.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/object.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/object.ML +(* Title: Pure/General/object.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/path.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Thy/path.ML +(* Title: Pure/General/path.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/position.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Thy/position.ML +(* Title: Pure/General/position.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/pretty.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Syntax/pretty.ML +(* Title: Pure/General/pretty.ML ID: $Id$ Author: Lawrence C Paulson Copyright 1991 University of Cambridge diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/scan.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Syntax/scan.ML +(* Title: Pure/General/scan.ML ID: $Id$ Author: Markus Wenzel and Tobias Nipkow, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/seq.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/seq.ML +(* Title: Pure/General/seq.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/source.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Syntax/source.ML +(* Title: Pure/General/source.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/symbol.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Syntax/symbol.ML +(* Title: Pure/General/symbol.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen diff -r f9aad8ccd590 -r caa439435666 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Wed Jan 13 15:14:47 1999 +0100 +++ b/src/Pure/General/table.ML Wed Jan 13 15:18:02 1999 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/table.ML +(* Title: Pure/General/table.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen