changeset 42463 | f270e3e18be5 |
parent 42150 | b0c0638c4aad |
child 54863 | 82acc20ded73 |
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Sat Apr 23 13:00:19 2011 +0200 @@ -9,8 +9,7 @@ imports SemilatAlg Opt begin -types - 's certificate = "'s list" +type_synonym 's certificate = "'s list" primrec merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" where "merge cert f r T pc [] x = x"