eliminated old CVS Ids;
authorwenzelm
Mon May 02 22:31:46 2011 +0200 (2011-05-02)
changeset 42637381fdcab0f36
parent 42636 41dff1b862bf
child 42638 a7a30721767a
eliminated old CVS Ids;
doc-src/Classes/Thy/ROOT.ML
doc-src/ERRATA.txt
doc-src/Functions/Makefile
doc-src/Functions/Thy/ROOT.ML
doc-src/HOL/HOL.tex
doc-src/HOL/logics-HOL.tex
doc-src/Inductive/Makefile
doc-src/Inductive/ind-defs-slides.tex
doc-src/Inductive/ind-defs.tex
doc-src/Intro/Makefile
doc-src/Intro/advanced.tex
doc-src/Intro/foundations.tex
doc-src/Intro/getting.tex
doc-src/Intro/intro.tex
doc-src/IsarOverview/Isar/document/Makefile
doc-src/IsarOverview/Makefile
doc-src/LaTeXsugar/Makefile
doc-src/Locales/Makefile
doc-src/Logics/CTT.tex
doc-src/Logics/LK.tex
doc-src/Logics/Makefile
doc-src/Logics/Sequents.tex
doc-src/Logics/logics.tex
doc-src/Logics/preface.tex
doc-src/Logics/syntax.tex
doc-src/Nitpick/Makefile
doc-src/Sledgehammer/Makefile
doc-src/TutorialI/Inductive/Even.thy
doc-src/TutorialI/Makefile
doc-src/TutorialI/Overview/Slides/PPRmyframes.sty
doc-src/TutorialI/Overview/Slides/prosper.cls
doc-src/TutorialI/Protocol/Event.thy
doc-src/TutorialI/Protocol/NS_Public.thy
doc-src/TutorialI/Protocol/ROOT.ML
doc-src/TutorialI/Protocol/protocol.tex
doc-src/TutorialI/Rules/Blast.thy
doc-src/TutorialI/Rules/Force.thy
doc-src/TutorialI/Rules/ROOT.ML
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/Functions.thy
doc-src/TutorialI/Sets/ROOT.ML
doc-src/TutorialI/Sets/Recur.thy
doc-src/TutorialI/Sets/Relations.thy
doc-src/TutorialI/Sets/sets.tex
doc-src/ZF/If.thy
doc-src/ZF/Makefile
doc-src/ZF/ROOT.ML
doc-src/ZF/ZF.tex
doc-src/ZF/logics-ZF.tex
     1.1 --- a/doc-src/Classes/Thy/ROOT.ML	Mon May 02 22:19:28 2011 +0200
     1.2 +++ b/doc-src/Classes/Thy/ROOT.ML	Mon May 02 22:31:46 2011 +0200
     1.3 @@ -1,6 +1,2 @@
     1.4 -
     1.5 -(* $Id$ *)
     1.6 -
     1.7  no_document use_thy "Setup";
     1.8 -
     1.9  use_thy "Classes";
     2.1 --- a/doc-src/ERRATA.txt	Mon May 02 22:19:28 2011 +0200
     2.2 +++ b/doc-src/ERRATA.txt	Mon May 02 22:31:46 2011 +0200
     2.3 @@ -1,4 +1,3 @@
     2.4 -$Id$
     2.5  ERRATA in the book "Isabelle: A Generic Theorem Prover"
     2.6  by Lawrence C. Paulson (contributions by Tobias Nipkow)
     2.7  
     3.1 --- a/doc-src/Functions/Makefile	Mon May 02 22:19:28 2011 +0200
     3.2 +++ b/doc-src/Functions/Makefile	Mon May 02 22:31:46 2011 +0200
     3.3 @@ -1,6 +1,3 @@
     3.4 -#
     3.5 -# $Id$
     3.6 -#
     3.7  
     3.8  ## targets
     3.9  
     4.1 --- a/doc-src/Functions/Thy/ROOT.ML	Mon May 02 22:19:28 2011 +0200
     4.2 +++ b/doc-src/Functions/Thy/ROOT.ML	Mon May 02 22:31:46 2011 +0200
     4.3 @@ -1,4 +1,1 @@
     4.4 -
     4.5 -(* $Id$ *)
     4.6 -
     4.7  use_thy "Functions";
     5.1 --- a/doc-src/HOL/HOL.tex	Mon May 02 22:19:28 2011 +0200
     5.2 +++ b/doc-src/HOL/HOL.tex	Mon May 02 22:31:46 2011 +0200
     5.3 @@ -1,4 +1,3 @@
     5.4 -%% $Id$
     5.5  \chapter{Higher-Order Logic}
     5.6  \index{higher-order logic|(}
     5.7  \index{HOL system@{\sc hol} system}
     6.1 --- a/doc-src/HOL/logics-HOL.tex	Mon May 02 22:19:28 2011 +0200
     6.2 +++ b/doc-src/HOL/logics-HOL.tex	Mon May 02 22:31:46 2011 +0200
     6.3 @@ -1,4 +1,3 @@
     6.4 -%% $Id$
     6.5  \documentclass[12pt,a4paper]{report}
     6.6  \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     6.7  \usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
     7.1 --- a/doc-src/Inductive/Makefile	Mon May 02 22:19:28 2011 +0200
     7.2 +++ b/doc-src/Inductive/Makefile	Mon May 02 22:31:46 2011 +0200
     7.3 @@ -1,6 +1,3 @@
     7.4 -#
     7.5 -# $Id$
     7.6 -#
     7.7  
     7.8  ## targets
     7.9  
     8.1 --- a/doc-src/Inductive/ind-defs-slides.tex	Mon May 02 22:19:28 2011 +0200
     8.2 +++ b/doc-src/Inductive/ind-defs-slides.tex	Mon May 02 22:31:46 2011 +0200
     8.3 @@ -1,6 +1,5 @@
     8.4  %process by     latex ind-defs-slides; dvips -Plime ind-defs-slides
     8.5  %               ghostview -magstep -2 -landscape ind-defs-slides.ps
     8.6 -%  $Id$
     8.7  \documentclass[a4,slidesonly,semlayer]{seminar}
     8.8  
     8.9  \usepackage{fancybox}
     9.1 --- a/doc-src/Inductive/ind-defs.tex	Mon May 02 22:19:28 2011 +0200
     9.2 +++ b/doc-src/Inductive/ind-defs.tex	Mon May 02 22:31:46 2011 +0200
     9.3 @@ -1,4 +1,3 @@
     9.4 -%% $Id$
     9.5  \documentclass[12pt,a4paper]{article}
     9.6  \usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup}
     9.7  
    10.1 --- a/doc-src/Intro/Makefile	Mon May 02 22:19:28 2011 +0200
    10.2 +++ b/doc-src/Intro/Makefile	Mon May 02 22:31:46 2011 +0200
    10.3 @@ -1,6 +1,3 @@
    10.4 -#
    10.5 -# $Id$
    10.6 -#
    10.7  
    10.8  ## targets
    10.9  
    11.1 --- a/doc-src/Intro/advanced.tex	Mon May 02 22:19:28 2011 +0200
    11.2 +++ b/doc-src/Intro/advanced.tex	Mon May 02 22:31:46 2011 +0200
    11.3 @@ -1,4 +1,3 @@
    11.4 -%% $Id$
    11.5  \part{Advanced Methods}
    11.6  Before continuing, it might be wise to try some of your own examples in
    11.7  Isabelle, reinforcing your knowledge of the basic functions.
    12.1 --- a/doc-src/Intro/foundations.tex	Mon May 02 22:19:28 2011 +0200
    12.2 +++ b/doc-src/Intro/foundations.tex	Mon May 02 22:31:46 2011 +0200
    12.3 @@ -1,5 +1,3 @@
    12.4 -%% $Id$
    12.5 -
    12.6  \part{Foundations} 
    12.7  The following sections discuss Isabelle's logical foundations in detail:
    12.8  representing logical syntax in the typed $\lambda$-calculus; expressing
    13.1 --- a/doc-src/Intro/getting.tex	Mon May 02 22:19:28 2011 +0200
    13.2 +++ b/doc-src/Intro/getting.tex	Mon May 02 22:31:46 2011 +0200
    13.3 @@ -1,4 +1,3 @@
    13.4 -%% $Id$
    13.5  \part{Using Isabelle from the ML Top-Level}\label{chap:getting}
    13.6  
    13.7  Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.  
    14.1 --- a/doc-src/Intro/intro.tex	Mon May 02 22:19:28 2011 +0200
    14.2 +++ b/doc-src/Intro/intro.tex	Mon May 02 22:31:46 2011 +0200
    14.3 @@ -1,7 +1,6 @@
    14.4  \documentclass[12pt,a4paper]{article}
    14.5  \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
    14.6  
    14.7 -%% $Id$
    14.8  %% run    bibtex intro         to prepare bibliography
    14.9  %% run    ../sedindex intro    to prepare index file
   14.10  %prth *(\(.*\));          \1;      
    15.1 --- a/doc-src/IsarOverview/Isar/document/Makefile	Mon May 02 22:19:28 2011 +0200
    15.2 +++ b/doc-src/IsarOverview/Isar/document/Makefile	Mon May 02 22:31:46 2011 +0200
    15.3 @@ -1,6 +1,3 @@
    15.4 -#
    15.5 -# $Id$
    15.6 -#
    15.7  
    15.8  ## targets
    15.9  
    16.1 --- a/doc-src/IsarOverview/Makefile	Mon May 02 22:19:28 2011 +0200
    16.2 +++ b/doc-src/IsarOverview/Makefile	Mon May 02 22:31:46 2011 +0200
    16.3 @@ -1,6 +1,3 @@
    16.4 -#
    16.5 -# $Id$
    16.6 -#
    16.7  
    16.8  ## targets
    16.9  
    17.1 --- a/doc-src/LaTeXsugar/Makefile	Mon May 02 22:19:28 2011 +0200
    17.2 +++ b/doc-src/LaTeXsugar/Makefile	Mon May 02 22:31:46 2011 +0200
    17.3 @@ -1,6 +1,3 @@
    17.4 -#
    17.5 -# $Id$
    17.6 -#
    17.7  
    17.8  ## targets
    17.9  
    18.1 --- a/doc-src/Locales/Makefile	Mon May 02 22:19:28 2011 +0200
    18.2 +++ b/doc-src/Locales/Makefile	Mon May 02 22:31:46 2011 +0200
    18.3 @@ -1,6 +1,3 @@
    18.4 -#
    18.5 -# $Id$
    18.6 -#
    18.7  
    18.8  ## targets
    18.9  
    19.1 --- a/doc-src/Logics/CTT.tex	Mon May 02 22:19:28 2011 +0200
    19.2 +++ b/doc-src/Logics/CTT.tex	Mon May 02 22:31:46 2011 +0200
    19.3 @@ -1,4 +1,3 @@
    19.4 -%% $Id$
    19.5  \chapter{Constructive Type Theory}
    19.6  \index{Constructive Type Theory|(}
    19.7  
    20.1 --- a/doc-src/Logics/LK.tex	Mon May 02 22:19:28 2011 +0200
    20.2 +++ b/doc-src/Logics/LK.tex	Mon May 02 22:31:46 2011 +0200
    20.3 @@ -1,4 +1,3 @@
    20.4 -%% $Id$
    20.5  \chapter{First-Order Sequent Calculus}
    20.6  \index{sequent calculus|(}
    20.7  
    21.1 --- a/doc-src/Logics/Makefile	Mon May 02 22:19:28 2011 +0200
    21.2 +++ b/doc-src/Logics/Makefile	Mon May 02 22:31:46 2011 +0200
    21.3 @@ -1,6 +1,3 @@
    21.4 -#
    21.5 -# $Id$
    21.6 -#
    21.7  
    21.8  ## targets
    21.9  
    22.1 --- a/doc-src/Logics/Sequents.tex	Mon May 02 22:19:28 2011 +0200
    22.2 +++ b/doc-src/Logics/Sequents.tex	Mon May 02 22:31:46 2011 +0200
    22.3 @@ -1,4 +1,3 @@
    22.4 -%% $Id$
    22.5  \chapter{Defining A Sequent-Based Logic}
    22.6  \label{chap:sequents}
    22.7  
    23.1 --- a/doc-src/Logics/logics.tex	Mon May 02 22:19:28 2011 +0200
    23.2 +++ b/doc-src/Logics/logics.tex	Mon May 02 22:31:46 2011 +0200
    23.3 @@ -1,4 +1,3 @@
    23.4 -%% $Id$
    23.5  \documentclass[12pt,a4paper]{report}
    23.6  \usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
    23.7  
    24.1 --- a/doc-src/Logics/preface.tex	Mon May 02 22:19:28 2011 +0200
    24.2 +++ b/doc-src/Logics/preface.tex	Mon May 02 22:31:46 2011 +0200
    24.3 @@ -1,4 +1,3 @@
    24.4 -%% $Id$
    24.5  \chapter*{Preface}
    24.6  Several logics come with Isabelle.  Many of them are sufficiently developed
    24.7  to serve as comfortable reasoning environments.  They are also good
    25.1 --- a/doc-src/Logics/syntax.tex	Mon May 02 22:19:28 2011 +0200
    25.2 +++ b/doc-src/Logics/syntax.tex	Mon May 02 22:31:46 2011 +0200
    25.3 @@ -1,4 +1,3 @@
    25.4 -%% $Id$
    25.5  %% THIS FILE IS COMMON TO ALL LOGIC MANUALS
    25.6  
    25.7  \chapter{Syntax definitions}
    26.1 --- a/doc-src/Nitpick/Makefile	Mon May 02 22:19:28 2011 +0200
    26.2 +++ b/doc-src/Nitpick/Makefile	Mon May 02 22:31:46 2011 +0200
    26.3 @@ -1,6 +1,3 @@
    26.4 -#
    26.5 -# $Id$
    26.6 -#
    26.7  
    26.8  ## targets
    26.9  
    27.1 --- a/doc-src/Sledgehammer/Makefile	Mon May 02 22:19:28 2011 +0200
    27.2 +++ b/doc-src/Sledgehammer/Makefile	Mon May 02 22:31:46 2011 +0200
    27.3 @@ -1,6 +1,3 @@
    27.4 -#
    27.5 -# $Id$
    27.6 -#
    27.7  
    27.8  ## targets
    27.9  
    28.1 --- a/doc-src/TutorialI/Inductive/Even.thy	Mon May 02 22:19:28 2011 +0200
    28.2 +++ b/doc-src/TutorialI/Inductive/Even.thy	Mon May 02 22:31:46 2011 +0200
    28.3 @@ -1,4 +1,3 @@
    28.4 -(* ID:         $Id$ *)
    28.5  (*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*)
    28.6  
    28.7  section{* The Set of Even Numbers *}
    29.1 --- a/doc-src/TutorialI/Makefile	Mon May 02 22:19:28 2011 +0200
    29.2 +++ b/doc-src/TutorialI/Makefile	Mon May 02 22:31:46 2011 +0200
    29.3 @@ -1,6 +1,3 @@
    29.4 -#
    29.5 -# $Id$
    29.6 -#
    29.7  
    29.8  ## targets
    29.9  
    30.1 --- a/doc-src/TutorialI/Overview/Slides/PPRmyframes.sty	Mon May 02 22:19:28 2011 +0200
    30.2 +++ b/doc-src/TutorialI/Overview/Slides/PPRmyframes.sty	Mon May 02 22:31:46 2011 +0200
    30.3 @@ -26,13 +26,11 @@
    30.4  % ON AN "AS IS" BASIS, AND THE AUTHOR HAS NO OBLIGATION TO
    30.5  % PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
    30.6  %
    30.7 -% CVSId : $Id$
    30.8  %==============================================================================
    30.9  \NeedsTeXFormat{LaTeX2e}[1995/12/01]
   30.10  \ProvidesPackage{PPRmyframes}[2000/04/18]
   30.11  \typeout{`Frames' style for prosper ---}
   30.12  \typeout{(c) 2000 Frederic Goualard, IRIN, France}
   30.13 -\typeout{CVSId: $Id$}
   30.14  \typeout{ }
   30.15  
   30.16  \RequirePackage{semhelv}
    31.1 --- a/doc-src/TutorialI/Overview/Slides/prosper.cls	Mon May 02 22:19:28 2011 +0200
    31.2 +++ b/doc-src/TutorialI/Overview/Slides/prosper.cls	Mon May 02 22:31:46 2011 +0200
    31.3 @@ -25,14 +25,12 @@
    31.4  % ON AN "AS IS" BASIS, AND THE AUTHOR HAS NO OBLIGATION TO
    31.5  % PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
    31.6  %
    31.7 -% CVSId : $Id$
    31.8  %==============================================================================
    31.9  
   31.10  \def\Prosper@Version{1.1}
   31.11  \NeedsTeXFormat{LaTeX2e}[1995/12/01]
   31.12  \ProvidesClass{prosper}[2001/01/23, v. \Prosper@Version]
   31.13  \typeout{(c) 2000 Frederic Goualard, CWI, The Netherlands}
   31.14 -\typeout{CVSId: $Id$}
   31.15  \typeout{ }
   31.16  
   31.17  \newif\ifDVItoPS
    32.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Mon May 02 22:19:28 2011 +0200
    32.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Mon May 02 22:31:46 2011 +0200
    32.3 @@ -1,5 +1,4 @@
    32.4  (*  Title:      HOL/Auth/Event
    32.5 -    ID:         $Id$
    32.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    32.7      Copyright   1996  University of Cambridge
    32.8  
    33.1 --- a/doc-src/TutorialI/Protocol/NS_Public.thy	Mon May 02 22:19:28 2011 +0200
    33.2 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy	Mon May 02 22:31:46 2011 +0200
    33.3 @@ -1,5 +1,4 @@
    33.4  (*  Title:      HOL/Auth/NS_Public
    33.5 -    ID:         $Id$
    33.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.7      Copyright   1996  University of Cambridge
    33.8  
    34.1 --- a/doc-src/TutorialI/Protocol/ROOT.ML	Mon May 02 22:19:28 2011 +0200
    34.2 +++ b/doc-src/TutorialI/Protocol/ROOT.ML	Mon May 02 22:31:46 2011 +0200
    34.3 @@ -1,5 +1,4 @@
    34.4 -(* ID:         $Id$ 
    34.5 -
    34.6 +(*
    34.7  To update:
    34.8  cp /home/lcp/isabelle/Repos/HOL/Auth/{Message.thy,Message_lemmas.ML,Event.thy,Event_lemmas.ML,Public.thy,Public_lemmas.ML,NS_Public.thy} .
    34.9  *)
    35.1 --- a/doc-src/TutorialI/Protocol/protocol.tex	Mon May 02 22:19:28 2011 +0200
    35.2 +++ b/doc-src/TutorialI/Protocol/protocol.tex	Mon May 02 22:31:46 2011 +0200
    35.3 @@ -1,4 +1,3 @@
    35.4 -% $Id$
    35.5  \chapter{Case Study: Verifying a Security Protocol}
    35.6  \label{chap:crypto}
    35.7  
    36.1 --- a/doc-src/TutorialI/Rules/Blast.thy	Mon May 02 22:19:28 2011 +0200
    36.2 +++ b/doc-src/TutorialI/Rules/Blast.thy	Mon May 02 22:31:46 2011 +0200
    36.3 @@ -1,4 +1,3 @@
    36.4 -(* ID:         $Id$ *)
    36.5  theory Blast imports Main begin
    36.6  
    36.7  lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y))))   =    
    37.1 --- a/doc-src/TutorialI/Rules/Force.thy	Mon May 02 22:19:28 2011 +0200
    37.2 +++ b/doc-src/TutorialI/Rules/Force.thy	Mon May 02 22:31:46 2011 +0200
    37.3 @@ -1,4 +1,3 @@
    37.4 -(* ID:         $Id$ *)
    37.5  theory Force imports Main begin 
    37.6    (*Use Divides rather than Main to experiment with the first proof.
    37.7      Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
    38.1 --- a/doc-src/TutorialI/Rules/ROOT.ML	Mon May 02 22:19:28 2011 +0200
    38.2 +++ b/doc-src/TutorialI/Rules/ROOT.ML	Mon May 02 22:31:46 2011 +0200
    38.3 @@ -1,4 +1,3 @@
    38.4 -(* ID:         $Id$ *)
    38.5  use_thy "Basic";
    38.6  use_thy "Blast";
    38.7  use_thy "Force";
    39.1 --- a/doc-src/TutorialI/Rules/rules.tex	Mon May 02 22:19:28 2011 +0200
    39.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Mon May 02 22:31:46 2011 +0200
    39.3 @@ -1,4 +1,3 @@
    39.4 -% $Id$
    39.5  %!TEX root = ../tutorial.tex
    39.6  \chapter{The Rules of the Game}
    39.7  \label{chap:rules}
    40.1 --- a/doc-src/TutorialI/Sets/Functions.thy	Mon May 02 22:19:28 2011 +0200
    40.2 +++ b/doc-src/TutorialI/Sets/Functions.thy	Mon May 02 22:31:46 2011 +0200
    40.3 @@ -1,4 +1,3 @@
    40.4 -(* ID:         $Id$ *)
    40.5  theory Functions imports Main begin
    40.6  
    40.7  ML "Pretty.margin_default := 64"
    41.1 --- a/doc-src/TutorialI/Sets/ROOT.ML	Mon May 02 22:19:28 2011 +0200
    41.2 +++ b/doc-src/TutorialI/Sets/ROOT.ML	Mon May 02 22:31:46 2011 +0200
    41.3 @@ -1,4 +1,3 @@
    41.4 -(* ID:         $Id$ *)
    41.5  use_thy "Examples";
    41.6  use_thy "Functions";
    41.7  use_thy "Relations";
    42.1 --- a/doc-src/TutorialI/Sets/Recur.thy	Mon May 02 22:19:28 2011 +0200
    42.2 +++ b/doc-src/TutorialI/Sets/Recur.thy	Mon May 02 22:31:46 2011 +0200
    42.3 @@ -1,4 +1,3 @@
    42.4 -(* ID:         $Id$ *)
    42.5  theory Recur imports Main begin
    42.6  
    42.7  ML "Pretty.margin_default := 64"
    43.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Mon May 02 22:19:28 2011 +0200
    43.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Mon May 02 22:31:46 2011 +0200
    43.3 @@ -1,4 +1,3 @@
    43.4 -(* ID:         $Id$ *)
    43.5  theory Relations imports Main begin
    43.6  
    43.7  ML "Pretty.margin_default := 64"
    44.1 --- a/doc-src/TutorialI/Sets/sets.tex	Mon May 02 22:19:28 2011 +0200
    44.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Mon May 02 22:31:46 2011 +0200
    44.3 @@ -1,4 +1,3 @@
    44.4 -% $Id$
    44.5  \chapter{Sets, Functions and Relations}
    44.6  
    44.7  This chapter describes the formalization of typed set theory, which is
    45.1 --- a/doc-src/ZF/If.thy	Mon May 02 22:19:28 2011 +0200
    45.2 +++ b/doc-src/ZF/If.thy	Mon May 02 22:31:46 2011 +0200
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      FOL/ex/If.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    45.7      Copyright   1991  University of Cambridge
    45.8  
    46.1 --- a/doc-src/ZF/Makefile	Mon May 02 22:19:28 2011 +0200
    46.2 +++ b/doc-src/ZF/Makefile	Mon May 02 22:31:46 2011 +0200
    46.3 @@ -1,6 +1,3 @@
    46.4 -#
    46.5 -# $Id$
    46.6 -#
    46.7  
    46.8  ## targets
    46.9  
    47.1 --- a/doc-src/ZF/ROOT.ML	Mon May 02 22:19:28 2011 +0200
    47.2 +++ b/doc-src/ZF/ROOT.ML	Mon May 02 22:31:46 2011 +0200
    47.3 @@ -1,4 +1,3 @@
    47.4 -(* ID:         $Id$ *)
    47.5  use_thy "IFOL_examples";
    47.6  use_thy "FOL_examples";
    47.7  use_thy "ZF_examples";
    48.1 --- a/doc-src/ZF/ZF.tex	Mon May 02 22:19:28 2011 +0200
    48.2 +++ b/doc-src/ZF/ZF.tex	Mon May 02 22:31:46 2011 +0200
    48.3 @@ -1,4 +1,3 @@
    48.4 -%% $Id$
    48.5  \chapter{Zermelo-Fraenkel Set Theory}
    48.6  \index{set theory|(}
    48.7  
    49.1 --- a/doc-src/ZF/logics-ZF.tex	Mon May 02 22:19:28 2011 +0200
    49.2 +++ b/doc-src/ZF/logics-ZF.tex	Mon May 02 22:31:46 2011 +0200
    49.3 @@ -1,4 +1,3 @@
    49.4 -%% $Id$
    49.5  \documentclass[11pt,a4paper]{report}
    49.6  \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    49.7  \usepackage{graphicx,logics,../ttbox,../proof,latexsym}