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