src/HOL/TLA/Buffer/DBuffer.ML
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/TLA/Buffer/DBuffer.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/Buffer/DBuffer.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4  goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
     1.5  by (rewtac (action_rewrite DBDeq_visible));
     1.6  by (cut_facts_tac [DB_base] 1);
     1.7 -by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
     1.8 -                     addsimps2 [angle_def,DBDeq_def,Deq_def]));
     1.9 +by (old_auto_tac (db_css addSEs2 [base_enabled,enabledE] 
    1.10 +                         addsimps2 [angle_def,DBDeq_def,Deq_def]));
    1.11  qed "DBDeq_enabled";
    1.12  
    1.13  goal DBuffer.thy "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";