--- a/src/HOL/List.thy Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/List.thy Sat May 19 11:33:57 2007 +0200
@@ -17,7 +17,7 @@
subsection{*Basic list processing functions*}
consts
- "@" :: "'a list => 'a list => 'a list" (infixr 65)
+ append :: "'a list => 'a list => 'a list" (infixr "@" 65)
filter:: "('a => bool) => 'a list => 'a list"
concat:: "'a list list => 'a list"
foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
@@ -309,7 +309,7 @@
fun len (Const("List.list.Nil",_)) acc = acc
| len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
- | len (Const("List.op @",_) $ xs $ ys) acc = len xs (len ys acc)
+ | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
| len (Const("List.rev",_) $ xs) acc = len xs acc
| len (Const("List.map",_) $ _ $ xs) acc = len xs acc
| len t (ts,n) = (t::ts,n);
@@ -447,7 +447,7 @@
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
(case xs of Const("List.list.Nil",_) => cons | _ => last xs)
- | last (Const("List.op @",_) $ _ $ ys) = last ys
+ | last (Const("List.append",_) $ _ $ ys) = last ys
| last t = t;
fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
@@ -455,7 +455,7 @@
fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
(case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
- | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
+ | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
| butlast xs = Const("List.list.Nil",fastype_of xs);
val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
@@ -469,7 +469,7 @@
val lhs1 = butlast lhs and rhs1 = butlast rhs;
val Type(_,listT::_) = eqT
val appT = [listT,listT] ---> listT
- val app = Const("List.op @",appT)
+ val app = Const("List.append",appT)
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
val thm = Goal.prove (Simplifier.the_context ss) [] [] eq