--- a/src/HOL/IMP/Com.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Com.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,6 @@
(* Title: HOL/IMP/Com.thy
- ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Isar Version: Gerwin Klein, 2001
- Copyright 1994 TUM
+ Author: Gerwin Klein
*)
header "Syntax of Commands"
--- a/src/HOL/IMP/Denotation.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Denotation.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/Denotation.thy
- ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
*)
header "Denotational Semantics of Commands"
--- a/src/HOL/IMP/Examples.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Examples.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/Examples.thy
- ID: $Id$
Author: David von Oheimb, TUM
- Copyright 2000 TUM
*)
header "Examples"
--- a/src/HOL/IMP/Expr.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Expr.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/Expr.thy
- ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Copyright 1994 TUM
*)
header "Expressions"
--- a/src/HOL/IMP/Hoare.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/Hoare.thy
- ID: $Id$
Author: Tobias Nipkow
- Copyright 1995 TUM
*)
header "Inductive Definition of Hoare Logic"
--- a/src/HOL/IMP/Hoare_Den.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare_Den.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/IMP/Hoare_Def.thy
- ID: $Id$
Author: Tobias Nipkow
*)
--- a/src/HOL/IMP/Hoare_Op.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare_Op.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/IMP/Hoare_Op.thy
- ID: $Id$
Author: Tobias Nipkow
*)
--- a/src/HOL/IMP/ROOT.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/ROOT.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/ROOT.ML
- ID: $Id$
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
- Copyright 1995 TUM
Caveat: HOLCF/IMP depends on HOL/IMP
*)
--- a/src/HOL/IMP/VC.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/VC.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMP/VC.thy
- ID: $Id$
Author: Tobias Nipkow
- Copyright 1996 TUM
acom: annotated commands
vc: verification-conditions
--- a/src/HOL/IMPP/Com.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Com.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMPP/Com.thy
- ID: $Id$
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
- Copyright 1999 TUM
*)
header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
--- a/src/HOL/IMPP/EvenOdd.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMPP/EvenOdd.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TUM
+ Author: David von Oheimb, TUM
*)
header {* Example of mutually recursive procedures verified with Hoare logic *}
--- a/src/HOL/IMPP/Misc.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Misc.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMPP/Misc.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TUM
+ Author: David von Oheimb, TUM
*)
header {* Several examples for Hoare logic *}
--- a/src/HOL/IMPP/Natural.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Natural.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/IMPP/Natural.thy
- ID: $Id$
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
- Copyright 1999 TUM
*)
header {* Natural semantics of commands *}
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/Generate-HOL/GenHOL4Base.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/Generate-HOL/GenHOL4Prob.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory GenHOL4Prob imports GenHOL4Real begin
--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/Generate-HOL/GenHOL4Vec.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory GenHOL4Vec imports GenHOL4Base begin
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/Generate-HOL/GenHOL4Word32.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory GenHOL4Word32 imports GenHOL4Base begin;
--- a/src/HOL/Import/Generate-HOL/ROOT.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,3 @@
-(* Title: HOL/Import/Generate-HOL/ROOT.ML
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
-*)
-
use_thy "GenHOL4Prob";
use_thy "GenHOL4Vec";
use_thy "GenHOL4Word32";
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy
- ID: $Id$
- Author: Steven Obua (TU Muenchen)
+ Author: Steven Obua, TU Muenchen
*)
theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
--- a/src/HOL/Import/Generate-HOLLight/ROOT.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOLLight/ROOT.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,1 @@
-(* Title: HOL/Import/Generate-HOLLight/ROOT.ML
- ID: $Id$
- Author: Steven Obua and Sebastian Skalberg (TU Muenchen)
-*)
-
use_thy "GenHOLLight";
--- a/src/HOL/Import/HOL/HOL4.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOL/HOL4.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/HOL/HOL4.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin
--- a/src/HOL/Import/HOL4Syntax.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOL4Syntax.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,10 +1,11 @@
(* Title: HOL/Import/HOL4Syntax.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
-theory HOL4Syntax imports HOL4Setup
- uses "import_syntax.ML" begin
+theory HOL4Syntax
+imports HOL4Setup
+uses "import_syntax.ML"
+begin
ML {* HOL4ImportSyntax.setup() *}
--- a/src/HOL/Import/HOLLight/ROOT.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOLLight/ROOT.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,1 @@
-(* Title: HOL/Import/HOLLight/ROOT.ML
- ID: $Id$
-*)
-
use_thy "HOLLight";
--- a/src/HOL/Import/HOLLightCompat.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/HOLLightCompat.thy
- ID: $Id$
- Author: Steven Obua and Sebastian Skalberg (TU Muenchen)
+ Author: Steven Obua and Sebastian Skalberg, TU Muenchen
*)
theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
--- a/src/HOL/Import/MakeEqual.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/MakeEqual.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Import/MakeEqual.thy
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
+ Author: Sebastian Skalberg, TU Muenchen
*)
theory MakeEqual imports Main
--- a/src/HOL/Import/mono_scan.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/mono_scan.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/Import/mono_scan.ML
- ID: $Id$
Author: Steven Obua, TU Muenchen
- Monomorphic scanner combinators for monomorphic sequences.
+Monomorphic scanner combinators for monomorphic sequences.
*)
signature MONO_SCANNER =
--- a/src/HOL/Import/mono_seq.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/mono_seq.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/Import/mono_seq.ML
- ID: $Id$
Author: Steven Obua, TU Muenchen
- Monomorphic sequences.
+Monomorphic sequences.
*)
(* The trouble is that signature / structures cannot depend on type variable parameters ... *)
--- a/src/HOL/MicroJava/Comp/NatCanonify.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/Comp/NatCanonify.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/Comp/NatCanonify.thy
- ID: $Id$
Author: Martin Strecker
*)
--- a/src/HOL/MicroJava/J/JBasis.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/J/JBasis.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
header {*
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/J/JTypeSafe.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header {* \isaheader{Type Safety Proof} *}
--- a/src/HOL/MicroJava/J/Term.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/J/Term.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header {* \isaheader{Expressions and Statements} *}
--- a/src/HOL/MicroJava/J/TypeRel.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/J/TypeRel.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header {* \isaheader{Relations between Java Types} *}
--- a/src/HOL/MicroJava/J/Value.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/J/Value.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header {* \isaheader{Java Values} *}
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/JVM/JVMInstructions.thy
- ID: $Id$
- Author: Gerwin Klein
- Copyright 2000 Technische Universitaet Muenchen
+ Author: Gerwin Klein, Technische Universitaet Muenchen
*)
header {* \isaheader{Instructions of the JVM} *}
--- a/src/HOL/MicroJava/JVM/JVMState.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/MicroJava/JVM/JVMState.thy
- ID: $Id$
- Author: Cornelia Pusch, Gerwin Klein
- Copyright 1999 Technische Universitaet Muenchen
+ Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
*)
header {*
--- a/src/HOL/NSA/Filter.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NSA/Filter.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,9 +1,7 @@
-(* Title : Filter.thy
- ID : $Id$
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Conversion to Isar and new proofs by Lawrence C Paulson, 2004
- Conversion to locales by Brian Huffman, 2005
+(* Title: Filter.thy
+ Author: Jacques D. Fleuriot, University of Cambridge
+ Author: Lawrence C Paulson
+ Author: Brian Huffman
*)
header {* Filters and Ultrafilters *}
--- a/src/HOL/NSA/HLim.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NSA/HLim.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,6 @@
-(* Title : HLim.thy
- ID : $Id$
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+(* Title: HLim.thy
+ Author: Jacques D. Fleuriot, University of Cambridge
+ Author: Lawrence C Paulson
*)
header{* Limits and Continuity (Nonstandard) *}
--- a/src/HOL/NanoJava/AxSem.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/NanoJava/AxSem.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 2001 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header "Axiomatic Semantics"
--- a/src/HOL/NanoJava/Term.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/Term.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/NanoJava/Term.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 2001 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header "Statements and expression emulations"
--- a/src/HOL/NanoJava/TypeRel.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/NanoJava/TypeRel.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 2001 Technische Universitaet Muenchen
+ Author: David von Oheimb, Technische Universitaet Muenchen
*)
header "Type relations"
--- a/src/HOL/Nominal/Examples/CR.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory CR
imports Lam_Funs
begin
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Lambda_mu
imports "../Nominal"
begin
--- a/src/HOL/Nominal/Examples/Support.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Support
imports "../Nominal"
begin
--- a/src/HOL/Nominal/Examples/VC_Condition.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory VC_Condition
imports "../Nominal"
begin
--- a/src/HOL/Prolog/ROOT.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Prolog/ROOT.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/ROOT.ML
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
--- a/src/HOL/TLA/Buffer/Buffer.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: Buffer.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Buffer/Buffer.thy
+ Author: Stephan Merz, University of Munich
*)
header {* A simple FIFO buffer (synchronous communication, interleaving) *}
--- a/src/HOL/TLA/Buffer/DBuffer.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: DBuffer.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Buffer/DBuffer.thy
+ Author: Stephan Merz, University of Munich
*)
header {* Two FIFO buffers in a row, with interleaving assumption *}
--- a/src/HOL/TLA/Inc/Inc.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: TLA/Inc/Inc.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Inc/Inc.thy
+ Author: Stephan Merz, University of Munich
*)
header {* Lamport's "increment" example *}
--- a/src/HOL/TLA/Memory/MemClerk.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: MemClerk.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/MemClerk.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: specification of the memory clerk *}
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: MemClerkParameters.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/MemClerkParameters.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: Parameters of the memory clerk *}
--- a/src/HOL/TLA/Memory/Memory.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: Memory.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/Memory.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: Memory specification *}
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: MemoryImplementation.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/MemoryImplementation.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: Memory implementation *}
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: MemoryParameters.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/MemoryParameters.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: Memory parameters *}
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: ProcedureInterface.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/ProcedureInterface.thy
+ Author: Stephan Merz, University of Munich
*)
header {* Procedure interface for RPC-Memory components *}
--- a/src/HOL/TLA/Memory/RPC.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: RPC.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/RPC.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: RPC specification *}
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: RPCMemoryParams.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/RPCMemoryParams.thy
+ Author: Stephan Merz, University of Munich
*)
header {* Basic declarations for the RPC-memory example *}
--- a/src/HOL/TLA/Memory/RPCParameters.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
- File: RPCParameters.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
+(* Title: HOL/TLA/Memory/RPCParameters.thy
+ Author: Stephan Merz, University of Munich
*)
header {* RPC-Memory example: RPC parameters *}
--- a/src/HOL/Tools/TFL/dcterm.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/Tools/TFL/dcterm.ML
- ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
*)
(*---------------------------------------------------------------------------
--- a/src/HOL/Tools/TFL/thry.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/thry.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/Tools/TFL/thry.ML
- ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
*)
signature THRY =
--- a/src/HOL/Tools/TFL/utils.ML Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/utils.ML Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/Tools/TFL/utils.ML
- ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
Basic utilities.
*)
--- a/src/HOL/ex/Sudoku.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/ex/Sudoku.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
-(* Title: Sudoku.thy
- ID: $Id$
+(* Title: HOL/ex/Sudoku.thy
Author: Tjark Weber
Copyright 2005-2008
*)
--- a/src/HOL/ex/svc_test.thy Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/ex/svc_test.thy Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
header {* Demonstrating the interface SVC *}
theory svc_test