src/HOL/TLA/Buffer/Buffer.ML
changeset 14396 011a2a49d303
parent 13601 fd3e3d6b37b2
child 17309 c43ed29bd197
     1.1 --- a/src/HOL/TLA/Buffer/Buffer.ML	Thu Feb 19 10:40:28 2004 +0100
     1.2 +++ b/src/HOL/TLA/Buffer/Buffer.ML	Thu Feb 19 10:41:01 2004 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  (* ---------------------------- Data lemmas ---------------------------- *)
     1.6  
     1.7 -context List.thy;
     1.8 -goal List.thy "xs ~= [] --> tl xs ~= xs";
     1.9 +(*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
    1.10 +Goal "xs ~= [] --> tl xs ~= xs";
    1.11  by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
    1.12  qed_spec_mp "tl_not_self";
    1.13  context Buffer.thy;