src/HOL/MicroJava/DFA/SemilatAlg.thy
changeset 35109 0015a0a99ae9
parent 33954 1bc3b688548c
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 21:31:50 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 21:33:25 2010 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
     1.5  
     1.6  consts
     1.7 - "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
     1.8 +  plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
     1.9  primrec
    1.10    "[] ++_f y = y"
    1.11    "(x#xs) ++_f y = xs ++_f (x +_f y)"