# HG changeset patch # User huffman # Date 1266429622 28800 # Node ID e15040ae75d7561cfb305a92f8494df98ebda2ec # Parent bb1d1c6a10bb642d3694194f39f620f1470796c9 remove $ from all HOLCF files diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/FOCUS/Buffer_adm.thy --- a/src/HOLCF/FOCUS/Buffer_adm.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/FOCUS/Buffer_adm.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/FOCUS/Buffer_adm.thy - ID: $Id$ Author: David von Oheimb, TU Muenchen *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/FOCUS/FOCUS.thy --- a/src/HOLCF/FOCUS/FOCUS.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/FOCUS/FOCUS.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/FOCUS/FOCUS.thy - ID: $Id$ Author: David von Oheimb, TU Muenchen *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/ex/Stream_adm.thy - ID: $Id$ Author: David von Oheimb, TU Muenchen *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IMP/Denotational.thy --- a/src/HOLCF/IMP/Denotational.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IMP/Denotational.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IMP/Denotational.thy - ID: $Id$ Author: Tobias Nipkow and Robert Sandner, TUM Copyright 1996 TUM *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IMP/HoareEx.thy --- a/src/HOLCF/IMP/HoareEx.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IMP/HoareEx.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IMP/HoareEx.thy - ID: $Id$ Author: Tobias Nipkow, TUM Copyright 1997 TUM *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IMP/README.html --- a/src/HOLCF/IMP/README.html Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IMP/README.html Wed Feb 17 10:00:22 2010 -0800 @@ -1,7 +1,5 @@ - - diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IMP/ROOT.ML --- a/src/HOLCF/IMP/ROOT.ML Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IMP/ROOT.ML Wed Feb 17 10:00:22 2010 -0800 @@ -1,3 +1,1 @@ -(* $Id$ *) - use_thys ["HoareEx"]; diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Abschannel.thy --- a/src/HOLCF/IOA/ABP/Abschannel.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Abschannel.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Abschannel_finite.thy --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Abschannels.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Action.thy --- a/src/HOLCF/IOA/ABP/Action.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Action.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Action.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Check.ML Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Check.ML - ID: $Id$ Author: Olaf Mueller The Model Checker. diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOLCF/IOA/ABP/Correctness.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Correctness.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Env.thy --- a/src/HOLCF/IOA/ABP/Env.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Env.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Impl.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Impl.thy --- a/src/HOLCF/IOA/ABP/Impl.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Impl.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Impl.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Impl_finite.thy --- a/src/HOLCF/IOA/ABP/Impl_finite.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Impl.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Lemmas.thy --- a/src/HOLCF/IOA/ABP/Lemmas.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Lemmas.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Packet.thy --- a/src/HOLCF/IOA/ABP/Packet.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Packet.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Packet.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Receiver.thy --- a/src/HOLCF/IOA/ABP/Receiver.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Receiver.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Receiver.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Sender.thy --- a/src/HOLCF/IOA/ABP/Sender.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Sender.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Sender.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/ABP/Spec.thy --- a/src/HOLCF/IOA/ABP/Spec.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/ABP/Spec.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Spec.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Modelcheck/Cockpit.thy --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,6 +1,3 @@ - -(* $Id$ *) - theory Cockpit imports MuIOAOracle begin diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Modelcheck/ROOT.ML --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/Modelcheck/ROOT.ML - ID: $Id$ Author: Olaf Mueller and Tobias Hamberger, TU Muenchen Modelchecker setup for I/O automata. diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOLCF/IOA/NTP/Abschannel.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Abschannel.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Action.thy --- a/src/HOLCF/IOA/NTP/Action.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Action.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Action.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Correctness.thy --- a/src/HOLCF/IOA/NTP/Correctness.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Correctness.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Correctness.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Impl.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Lemmas.thy --- a/src/HOLCF/IOA/NTP/Lemmas.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Lemmas.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Multiset.thy --- a/src/HOLCF/IOA/NTP/Multiset.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Multiset.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Multiset.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Packet.thy --- a/src/HOLCF/IOA/NTP/Packet.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Packet.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Packet.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Receiver.thy --- a/src/HOLCF/IOA/NTP/Receiver.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Receiver.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Sender.thy --- a/src/HOLCF/IOA/NTP/Sender.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Sender.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Sender.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/NTP/Spec.thy --- a/src/HOLCF/IOA/NTP/Spec.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/NTP/Spec.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/README.html --- a/src/HOLCF/IOA/README.html Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/README.html Wed Feb 17 10:00:22 2010 -0800 @@ -1,7 +1,5 @@ - - diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Storage/Action.thy --- a/src/HOLCF/IOA/Storage/Action.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Storage/Action.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/ABP/Action.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Storage/Correctness.thy --- a/src/HOLCF/IOA/Storage/Correctness.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/example/Correctness.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Storage/Impl.thy --- a/src/HOLCF/IOA/Storage/Impl.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Storage/Impl.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/example/Spec.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/Storage/Spec.thy --- a/src/HOLCF/IOA/Storage/Spec.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/Storage/Spec.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/example/Spec.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Asig.thy --- a/src/HOLCF/IOA/meta_theory/Asig.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/meta_theory/Asig.thy - ID: $Id$ Author: Olaf Müller, Tobias Nipkow & Konrad Slind *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Automata.thy --- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Automata.thy - ID: $Id$ Author: Olaf Müller, Konrad Slind, Tobias Nipkow *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/CompoExecs.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/CompoScheds.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/CompoTraces.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Compositionality.thy --- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Compositionality.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Deadlock.thy --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Deadlock.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/IOA.thy --- a/src/HOLCF/IOA/meta_theory/IOA.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/IOA.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/LiveIOA.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Pred.thy --- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Pred.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/RefMappings.thy --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/RefMappings.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Seq.thy --- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Seq.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/ShortExecutions.thy --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/Simulations.thy --- a/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Simulations.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/TL.thy --- a/src/HOLCF/IOA/meta_theory/TL.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/TL.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/TLS.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOLCF/IOA/meta_theory/TLS.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/TLS.thy - ID: $Id$ Author: Olaf Müller *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/README.html --- a/src/HOLCF/README.html Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/README.html Wed Feb 17 10:00:22 2010 -0800 @@ -1,7 +1,5 @@ - - diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Dagstuhl.thy --- a/src/HOLCF/ex/Dagstuhl.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Dagstuhl.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Dagstuhl imports Stream begin diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Fix2.thy --- a/src/HOLCF/ex/Fix2.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Fix2.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/ex/Fix2.thy - ID: $Id$ Author: Franz Regensburger Show that fix is the unique least fixed-point operator. diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Focus_ex.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,3 @@ -(* $Id$ *) - (* Specification of the following loop back device diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Hoare.thy --- a/src/HOLCF/ex/Hoare.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Hoare.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/ex/hoare.thy - ID: $Id$ Author: Franz Regensburger Theory for an example by C.A.R. Hoare diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Loop.thy --- a/src/HOLCF/ex/Loop.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Loop.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/ex/Loop.thy - ID: $Id$ Author: Franz Regensburger *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/Stream.thy Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOLCF/ex/Stream.thy - ID: $Id$ Author: Franz Regensburger, David von Oheimb, Borislav Gajanovic *) diff -r bb1d1c6a10bb -r e15040ae75d7 src/HOLCF/ex/hoare.txt --- a/src/HOLCF/ex/hoare.txt Wed Feb 17 09:22:40 2010 -0800 +++ b/src/HOLCF/ex/hoare.txt Wed Feb 17 10:00:22 2010 -0800 @@ -1,5 +1,3 @@ -(* $Id$ *) - Proves about loops and tail-recursive functions ===============================================