src/HOL/TLA/Buffer/Buffer.ML

--- a/src/HOL/TLA/Buffer/Buffer.ML	Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.ML	Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(* 
+(*
     File:        Buffer.ML
+    ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1997 University of Munich
 
@@ -8,11 +9,10 @@
 
 (* ---------------------------- Data lemmas ---------------------------- *)
 
-(*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
+(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
 Goal "xs ~= [] --> tl xs ~= xs";
 by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
 qed_spec_mp "tl_not_self";
-context Buffer.thy;
 
 Addsimps [tl_not_self];
 
@@ -26,12 +26,12 @@
 (* Enabling condition for dequeue -- NOT NEEDED *)
 Goalw [temp_rewrite Deq_visible]
    "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])";
-by (force_tac (claset() addSEs [base_enabled,enabledE], 
+by (force_tac (claset() addSEs [base_enabled,enabledE],
                simpset() addsimps [Deq_def]) 1);
 qed "Deq_enabled";
 
 (* For the left-to-right implication, we don't need the base variable stuff *)
-Goalw [temp_rewrite Deq_visible] 
+Goalw [temp_rewrite Deq_visible]
    "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])";
 by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def]));
 qed "Deq_enabledE";