--- a/doc-src/Classes/Thy/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Classes/Thy/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,2 @@
-
-(* $Id$ *)
-
no_document use_thy "Setup";
-
use_thy "Classes";
--- a/doc-src/ERRATA.txt Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ERRATA.txt Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-$Id$
ERRATA in the book "Isabelle: A Generic Theorem Prover"
by Lawrence C. Paulson (contributions by Tobias Nipkow)
--- a/doc-src/Functions/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Functions/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Functions/Thy/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Functions/Thy/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
use_thy "Functions";
--- a/doc-src/HOL/HOL.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/HOL/HOL.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter{Higher-Order Logic}
\index{higher-order logic|(}
\index{HOL system@{\sc hol} system}
--- a/doc-src/HOL/logics-HOL.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/HOL/logics-HOL.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\documentclass[12pt,a4paper]{report}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
--- a/doc-src/Inductive/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Inductive/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Inductive/ind-defs-slides.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Inductive/ind-defs-slides.tex Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,5 @@
%process by latex ind-defs-slides; dvips -Plime ind-defs-slides
% ghostview -magstep -2 -landscape ind-defs-slides.ps
-% $Id$
\documentclass[a4,slidesonly,semlayer]{seminar}
\usepackage{fancybox}
--- a/doc-src/Inductive/ind-defs.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Inductive/ind-defs.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\documentclass[12pt,a4paper]{article}
\usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup}
--- a/doc-src/Intro/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Intro/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Intro/advanced.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Intro/advanced.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\part{Advanced Methods}
Before continuing, it might be wise to try some of your own examples in
Isabelle, reinforcing your knowledge of the basic functions.
--- a/doc-src/Intro/foundations.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Intro/foundations.tex Mon May 02 22:31:46 2011 +0200
@@ -1,5 +1,3 @@
-%% $Id$
-
\part{Foundations}
The following sections discuss Isabelle's logical foundations in detail:
representing logical syntax in the typed $\lambda$-calculus; expressing
--- a/doc-src/Intro/getting.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Intro/getting.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\part{Using Isabelle from the ML Top-Level}\label{chap:getting}
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.
--- a/doc-src/Intro/intro.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Intro/intro.tex Mon May 02 22:31:46 2011 +0200
@@ -1,7 +1,6 @@
\documentclass[12pt,a4paper]{article}
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
-%% $Id$
%% run bibtex intro to prepare bibliography
%% run ../sedindex intro to prepare index file
%prth *(\(.*\)); \1;
--- a/doc-src/IsarOverview/Isar/document/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/IsarOverview/Isar/document/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/IsarOverview/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/IsarOverview/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/LaTeXsugar/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/LaTeXsugar/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Locales/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Locales/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Logics/CTT.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/CTT.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter{Constructive Type Theory}
\index{Constructive Type Theory|(}
--- a/doc-src/Logics/LK.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/LK.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter{First-Order Sequent Calculus}
\index{sequent calculus|(}
--- a/doc-src/Logics/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Logics/Sequents.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/Sequents.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter{Defining A Sequent-Based Logic}
\label{chap:sequents}
--- a/doc-src/Logics/logics.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/logics.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\documentclass[12pt,a4paper]{report}
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
--- a/doc-src/Logics/preface.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/preface.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter*{Preface}
Several logics come with Isabelle. Many of them are sufficiently developed
to serve as comfortable reasoning environments. They are also good
--- a/doc-src/Logics/syntax.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Logics/syntax.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
%% THIS FILE IS COMMON TO ALL LOGIC MANUALS
\chapter{Syntax definitions}
--- a/doc-src/Nitpick/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Nitpick/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/Sledgehammer/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/Sledgehammer/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/TutorialI/Inductive/Even.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*)
section{* The Set of Even Numbers *}
--- a/doc-src/TutorialI/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/TutorialI/Overview/Slides/PPRmyframes.sty Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Overview/Slides/PPRmyframes.sty Mon May 02 22:31:46 2011 +0200
@@ -26,13 +26,11 @@
% ON AN "AS IS" BASIS, AND THE AUTHOR HAS NO OBLIGATION TO
% PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
%
-% CVSId : $Id$
%==============================================================================
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesPackage{PPRmyframes}[2000/04/18]
\typeout{`Frames' style for prosper ---}
\typeout{(c) 2000 Frederic Goualard, IRIN, France}
-\typeout{CVSId: $Id$}
\typeout{ }
\RequirePackage{semhelv}
--- a/doc-src/TutorialI/Overview/Slides/prosper.cls Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Overview/Slides/prosper.cls Mon May 02 22:31:46 2011 +0200
@@ -25,14 +25,12 @@
% ON AN "AS IS" BASIS, AND THE AUTHOR HAS NO OBLIGATION TO
% PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
%
-% CVSId : $Id$
%==============================================================================
\def\Prosper@Version{1.1}
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesClass{prosper}[2001/01/23, v. \Prosper@Version]
\typeout{(c) 2000 Frederic Goualard, CWI, The Netherlands}
-\typeout{CVSId: $Id$}
\typeout{ }
\newif\ifDVItoPS
--- a/doc-src/TutorialI/Protocol/Event.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy Mon May 02 22:31:46 2011 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Event
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
--- a/doc-src/TutorialI/Protocol/NS_Public.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Mon May 02 22:31:46 2011 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/NS_Public
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
--- a/doc-src/TutorialI/Protocol/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Protocol/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,5 +1,4 @@
-(* ID: $Id$
-
+(*
To update:
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} .
*)
--- a/doc-src/TutorialI/Protocol/protocol.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-% $Id$
\chapter{Case Study: Verifying a Security Protocol}
\label{chap:crypto}
--- a/doc-src/TutorialI/Rules/Blast.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Rules/Blast.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Blast imports Main begin
lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y)))) =
--- a/doc-src/TutorialI/Rules/Force.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Force imports Main begin
(*Use Divides rather than Main to experiment with the first proof.
Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
--- a/doc-src/TutorialI/Rules/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Rules/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
use_thy "Basic";
use_thy "Blast";
use_thy "Force";
--- a/doc-src/TutorialI/Rules/rules.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-% $Id$
%!TEX root = ../tutorial.tex
\chapter{The Rules of the Game}
\label{chap:rules}
--- a/doc-src/TutorialI/Sets/Functions.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Functions imports Main begin
ML "Pretty.margin_default := 64"
--- a/doc-src/TutorialI/Sets/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
use_thy "Examples";
use_thy "Functions";
use_thy "Relations";
--- a/doc-src/TutorialI/Sets/Recur.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Recur imports Main begin
ML "Pretty.margin_default := 64"
--- a/doc-src/TutorialI/Sets/Relations.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Relations imports Main begin
ML "Pretty.margin_default := 64"
--- a/doc-src/TutorialI/Sets/sets.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-% $Id$
\chapter{Sets, Functions and Relations}
This chapter describes the formalization of typed set theory, which is
--- a/doc-src/ZF/If.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ZF/If.thy Mon May 02 22:31:46 2011 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/If.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
--- a/doc-src/ZF/Makefile Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ZF/Makefile Mon May 02 22:31:46 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
--- a/doc-src/ZF/ROOT.ML Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ZF/ROOT.ML Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
use_thy "IFOL_examples";
use_thy "FOL_examples";
use_thy "ZF_examples";
--- a/doc-src/ZF/ZF.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ZF/ZF.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\chapter{Zermelo-Fraenkel Set Theory}
\index{set theory|(}
--- a/doc-src/ZF/logics-ZF.tex Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/ZF/logics-ZF.tex Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-%% $Id$
\documentclass[11pt,a4paper]{report}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
\usepackage{graphicx,logics,../ttbox,../proof,latexsym}