--- a/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 21:33:25 2010 +0100
@@ -19,9 +19,10 @@
esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
-syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
+abbreviation
+ lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
-translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
+ where "p <=(rA,rB) q == p <=_(le rA rB) q"
lemma unfold_lesub_prod:
"p <=(rA,rB) q == le rA rB p q"