src/HOL/TLA/Buffer/DBuffer.ML

--- a/src/HOL/TLA/Buffer/DBuffer.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -14,13 +14,13 @@
 
 
 (*** Proper initialization ***)
-goal DBuffer.thy "Init DBInit .-> Init (BInit inp qc out)";
+Goal "Init DBInit .-> Init (BInit inp qc out)";
 by (auto_tac (db_css addsimps2 [Init_def,DBInit_def,BInit_def]));
 qed "DBInit";
 
 
 (*** Step simulation ***)
-goal DBuffer.thy "[DBNext]_<inp,mid,out,q1,q2> .-> [Next inp qc out]_<inp,qc,out>";
+Goal "[DBNext]_<inp,mid,out,q1,q2> .-> [Next inp qc out]_<inp,qc,out>";
 by (rtac square_simulation 1);
 by (Action_simp_tac 1);
 by (action_simp_tac (simpset() addsimps hd_append::db_defs) [] [] 1);
@@ -30,22 +30,22 @@
 (*** Simulation of fairness ***)
 
 (* Compute enabledness predicates for DBDeq and DBPass actions *)
-goal DBuffer.thy "<DBDeq>_<inp,mid,out,q1,q2> .= DBDeq";
+Goal "<DBDeq>_<inp,mid,out,q1,q2> .= DBDeq";
 by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def]));
 qed "DBDeq_visible";
 
-goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
+Goal "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
 by (rewtac (action_rewrite DBDeq_visible));
 by (cut_facts_tac [DB_base] 1);
 by (old_auto_tac (db_css addSEs2 [base_enabled,enabledE] 
                          addsimps2 [angle_def,DBDeq_def,Deq_def]));
 qed "DBDeq_enabled";
 
-goal DBuffer.thy "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";
+Goal "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";
 by (auto_tac (db_css addsimps2 [angle_def,DBPass_def,Deq_def]));
 qed "DBPass_visible";
 
-goal DBuffer.thy "$Enabled (<DBPass>_<inp,mid,out,q1,q2>) .= ($q1 .~= .[])";
+Goal "$Enabled (<DBPass>_<inp,mid,out,q1,q2>) .= ($q1 .~= .[])";
 by (rewtac (action_rewrite DBPass_visible));
 by (cut_facts_tac [DB_base] 1);
 by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
@@ -73,7 +73,7 @@
 *)
 
 (* Condition (1a) *)
-goal DBuffer.thy 
+Goal 
   "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
 \  .-> ($qc .~= .[] .& $q2 .= .[] ~> $q2 .~= .[])";
 by (rtac WF1 1);
@@ -83,7 +83,7 @@
 qed "DBFair_1a";
 
 (* Condition (1) *)
-goal DBuffer.thy
+Goal
   "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
 \  .-> ($Enabled (<Deq inp qc out>_<inp,qc,out>) ~> $q2 .~= .[])";
 by (auto_tac (temp_css addSIs2 [leadsto_classical] addSEs2 [temp_conjimpE DBFair_1a]));
@@ -92,7 +92,7 @@
 qed "DBFair_1";
 
 (* Condition (2) *)
-goal DBuffer.thy
+Goal
   "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBDeq)_<inp,mid,out,q1,q2> \
 \  .-> ($q2 .~= .[] ~> DBDeq)";
 by (rtac WF_leadsto 1);
@@ -102,7 +102,7 @@
 qed "DBFair_2";
 
 (* High-level fairness *)
-goal DBuffer.thy
+Goal
   "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
 \                                 .& WF(DBDeq)_<inp,mid,out,q1,q2>  \ 
 \  .-> WF(Deq inp qc out)_<inp,qc,out>";
@@ -114,6 +114,6 @@
 qed "DBFair";
 
 (*** Main theorem ***)
-goalw DBuffer.thy [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out";
+Goalw [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out";
 by (auto_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair])));
 qed "DBuffer_impl_Buffer";