src/HOL/MicroJava/DFA/Product.thy
changeset 35109 0015a0a99ae9
parent 33954 1bc3b688548c
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 21:31:50 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 21:33:25 2010 +0100
     1.3 @@ -19,9 +19,10 @@
     1.4   esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
     1.5  "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
     1.6  
     1.7 -syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
     1.8 +abbreviation
     1.9 +  lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    1.10         ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
    1.11 -translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
    1.12 +  where "p <=(rA,rB) q == p <=_(le rA rB) q"
    1.13  
    1.14  lemma unfold_lesub_prod:
    1.15    "p <=(rA,rB) q == le rA rB p q"