--- a/src/HOL/MicroJava/DFA/Listn.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Thu Feb 11 00:45:02 2010 +0100
@@ -17,21 +17,24 @@
le :: "'a ord \<Rightarrow> ('a list)ord"
"le r == list_all2 (%x y. x <=_r y)"
-syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+abbreviation
+ lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "x <=[r] y == x <=_(le r) y"
+
+abbreviation
+ lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<[_] _)" [50, 0, 51] 50)
-translations
- "x <=[r] y" == "x <=_(Listn.le r) y"
- "x <[r] y" == "x <_(Listn.le r) y"
+ where "x <[r] y == x <_(le r) y"
constdefs
map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
"map2 f == (%xs ys. map (split f) (zip xs ys))"
-syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
+abbreviation
+ plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
("(_ /+[_] _)" [65, 0, 66] 65)
-translations "x +[f] y" == "x +_(map2 f) y"
+ where "x +[f] y == x +_(map2 f) y"
consts coalesce :: "'a err list \<Rightarrow> 'a list err"
primrec