--- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 11:31:15 2010 -0800
@@ -2864,8 +2864,8 @@
then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0"
by (auto simp add: algebra_simps)
- from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
- by (simp add: pochhammer_neq_0_mono)
+ from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
+ by (rule pochhammer_neq_0_mono)
{assume k0: "k = 0 \<or> n =0"
then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
using kn
--- a/src/HOL/Library/Ramsey.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOL/Library/Ramsey.thy Wed Feb 17 11:31:15 2010 -0800
@@ -111,7 +111,7 @@
have infYx': "infinite (Yx-{yx'})" using fields px by auto
with fields px yx' Suc.prems
have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
- by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY])
+ by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
from Suc.hyps [OF infYx' partfx']
obtain Y' and t'
where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
--- a/src/HOL/Library/Word.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOL/Library/Word.thy Wed Feb 17 11:31:15 2010 -0800
@@ -980,7 +980,8 @@
fix xs
assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
thus "norm_signed (\<zero>#xs) = \<zero>#xs"
- by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
+ by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
+ split: split_if_asm)
next
fix xs
assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
--- a/src/HOL/Library/Zorn.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOL/Library/Zorn.thy Wed Feb 17 11:31:15 2010 -0800
@@ -333,7 +333,7 @@
lemma antisym_init_seg_of:
"r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
-by(auto simp:init_seg_of_def)
+unfolding init_seg_of_def by safe
lemma Chain_init_seg_of_Union:
"R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/FOCUS/Buffer_adm.thy
- ID: $Id$
Author: David von Oheimb, TU Muenchen
*)
--- a/src/HOLCF/FOCUS/FOCUS.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/FOCUS/FOCUS.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/FOCUS/FOCUS.thy
- ID: $Id$
Author: David von Oheimb, TU Muenchen
*)
--- a/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/ex/Stream_adm.thy
- ID: $Id$
Author: David von Oheimb, TU Muenchen
*)
--- a/src/HOLCF/IMP/Denotational.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IMP/Denotational.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IMP/Denotational.thy
- ID: $Id$
Author: Tobias Nipkow and Robert Sandner, TUM
Copyright 1996 TUM
*)
--- a/src/HOLCF/IMP/HoareEx.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IMP/HoareEx.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IMP/HoareEx.thy
- ID: $Id$
Author: Tobias Nipkow, TUM
Copyright 1997 TUM
*)
--- a/src/HOLCF/IMP/README.html Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IMP/README.html Wed Feb 17 11:31:15 2010 -0800
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOLCF/IMP/ROOT.ML Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IMP/ROOT.ML Wed Feb 17 11:31:15 2010 -0800
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
use_thys ["HoareEx"];
--- a/src/HOLCF/IOA/ABP/Abschannel.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Abschannel.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Abschannel.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Abschannels.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Action.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Action.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Action.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Check.ML Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Check.ML Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Check.ML
- ID: $Id$
Author: Olaf Mueller
The Model Checker.
--- a/src/HOLCF/IOA/ABP/Correctness.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Correctness.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Env.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Env.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Impl.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Impl.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Impl_finite.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Lemmas.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Lemmas.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Packet.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Packet.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Packet.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Receiver.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Receiver.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Receiver.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Sender.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Sender.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Sender.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/ABP/Spec.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/ABP/Spec.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Spec.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
theory Cockpit
imports MuIOAOracle
begin
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Wed Feb 17 11:31:15 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.
--- a/src/HOLCF/IOA/NTP/Abschannel.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Abschannel.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Abschannel.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/NTP/Action.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Action.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Action.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Correctness.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Correctness.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Impl.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Impl.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Lemmas.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Lemmas.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Multiset.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Multiset.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Packet.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Packet.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Packet.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Receiver.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Receiver.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Sender.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Sender.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Sender.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/NTP/Spec.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/NTP/Spec.thy
- ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/README.html Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/README.html Wed Feb 17 11:31:15 2010 -0800
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOLCF/IOA/Storage/Action.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Storage/Action.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/ABP/Action.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/Storage/Correctness.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/example/Correctness.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/Storage/Impl.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Storage/Impl.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/example/Spec.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/Storage/Spec.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/Storage/Spec.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/example/Spec.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Asig.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/IOA/meta_theory/Asig.thy
- ID: $Id$
Author: Olaf Müller, Tobias Nipkow & Konrad Slind
*)
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Automata.thy
- ID: $Id$
Author: Olaf Müller, Konrad Slind, Tobias Nipkow
*)
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Deadlock.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/IOA.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Pred.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Seq.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Simulations.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/TL.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
- ID: $Id$
Author: Olaf Müller
*)
--- a/src/HOLCF/README.html Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/README.html Wed Feb 17 11:31:15 2010 -0800
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- a/src/HOLCF/ex/Dagstuhl.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Dagstuhl
imports Stream
begin
--- a/src/HOLCF/ex/Fix2.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Fix2.thy Wed Feb 17 11:31:15 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.
--- a/src/HOLCF/ex/Focus_ex.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Focus_ex.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
(* Specification of the following loop back device
--- a/src/HOLCF/ex/Hoare.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Feb 17 11:31:15 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
--- a/src/HOLCF/ex/Loop.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/ex/Loop.thy
- ID: $Id$
Author: Franz Regensburger
*)
--- a/src/HOLCF/ex/Stream.thy Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/ex/Stream.thy
- ID: $Id$
Author: Franz Regensburger, David von Oheimb, Borislav Gajanovic
*)
--- a/src/HOLCF/ex/hoare.txt Wed Feb 17 18:56:34 2010 +0100
+++ b/src/HOLCF/ex/hoare.txt Wed Feb 17 11:31:15 2010 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
Proves about loops and tail-recursive functions
===============================================