--- a/NEWS Sat May 19 11:33:34 2007 +0200
+++ b/NEWS Sat May 19 11:33:57 2007 +0200
@@ -530,6 +530,10 @@
*** HOL ***
+* constant "List.op @" now named "List.append". Use ML antiquotations
+@{const_name List.append} or @{term " ... @ ... "} to circumvent
+possible incompatibilities when working on ML level.
+
* Constant renames due to introduction of canonical name prefixing for
class package:
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat May 19 11:33:57 2007 +0200
@@ -235,7 +235,7 @@
REVERSE > List.rev
LAST > List.last
FRONT > List.butlast
- APPEND > "List.op @"
+ APPEND > List.append
FLAT > List.concat
LENGTH > Nat.size
REPLICATE > List.replicate
--- a/src/HOL/Import/HOL/list.imp Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Import/HOL/list.imp Sat May 19 11:33:57 2007 +0200
@@ -33,7 +33,7 @@
"EXISTS" > "HOL4Compat.list_exists"
"EVERY" > "List.list_all"
"CONS" > "List.list.Cons"
- "APPEND" > "List.op @"
+ "APPEND" > "List.append"
thm_maps
"list_size_def" > "HOL4Compat.list_size_def"
--- a/src/HOL/Induct/SList.thy Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Induct/SList.thy Sat May 19 11:33:57 2007 +0200
@@ -159,6 +159,10 @@
map :: "('a=>'b) => ('a list => 'b list)" where
"map f xs = list_rec xs [] (%x l r. f(x)#r)"
+no_syntax
+ append :: "'a list => 'a list => 'a list" (infixr "@" 65)
+hide const "List.append"
+
definition
append :: "['a list, 'a list] => 'a list" (infixr "@" 65) where
"xs@ys = list_rec xs ys (%x l r. x#r)"
--- 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
--- a/src/HOL/Nominal/nominal_atoms.ML Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat May 19 11:33:57 2007 +0200
@@ -204,7 +204,7 @@
val pi2 = Free ("pi2", mk_permT T);
val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
val cnil = Const ("List.list.Nil", mk_permT T);
- val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
+ val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
(* nil axiom *)
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
--- a/src/HOL/Nominal/nominal_package.ML Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Sat May 19 11:33:57 2007 +0200
@@ -206,7 +206,7 @@
val fresh_def = thm "fresh_def";
val supp_def = thm "supp_def";
val rev_simps = thms "rev.simps";
-val app_simps = thms "op @.simps";
+val app_simps = thms "append.simps";
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
@@ -402,7 +402,7 @@
(map (fn ((s, T), x) =>
let val perm = Const (s, permT --> T --> T)
in HOLogic.mk_eq
- (perm $ (Const ("List.op @", permT --> permT --> permT) $
+ (perm $ (Const ("List.append", permT --> permT --> permT) $
pi1 $ pi2) $ Free (x, T),
perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
end)
--- a/src/HOL/Tools/refute.ML Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Tools/refute.ML Sat May 19 11:33:57 2007 +0200
@@ -704,7 +704,7 @@
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
| Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const ("List.op @", _) => t
+ | Const ("List.append", _) => t
| Const ("Lfp.lfp", _) => t
| Const ("Gfp.gfp", _) => t
| Const ("fst", _) => t
@@ -895,7 +895,7 @@
| Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms (axs, T)
- | Const ("List.op @", T) => collect_type_axioms (axs, T)
+ | Const ("List.append", T) => collect_type_axioms (axs, T)
| Const ("Lfp.lfp", T) => collect_type_axioms (axs, T)
| Const ("Gfp.gfp", T) => collect_type_axioms (axs, T)
| Const ("fst", T) => collect_type_axioms (axs, T)
@@ -2727,13 +2727,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'op @' could in principle be interpreted with *)
+ (* only an optimization: 'append' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
fun List_append_interpreter thy model args t =
case t of
- Const ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun",
+ Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun",
[Type ("List.list", [_]), Type ("List.list", [_])])])) =>
let
val (i_elem, _, _) = interpret thy model
@@ -3215,7 +3215,7 @@
add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #>
add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #>
add_interpreter "Nat_HOL.times" Nat_times_interpreter #>
- add_interpreter "List.op @" List_append_interpreter #>
+ add_interpreter "List.append" List_append_interpreter #>
add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
add_interpreter "fst" Product_Type_fst_interpreter #>
--- a/src/HOL/Tools/res_clause.ML Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML Sat May 19 11:33:57 2007 +0200
@@ -117,7 +117,7 @@
("op :", "in"),
("op Un", "union"),
("op Int", "inter"),
- ("List.op @", "append"),
+ ("List.append", "append"),
("ATP_Linkup.fequal", "fequal"),
("ATP_Linkup.COMBI", "COMBI"),
("ATP_Linkup.COMBK", "COMBK"),