src/HOL/MicroJava/DFA/Semilat.thy
changeset 42463 f270e3e18be5
parent 42150 b0c0638c4aad
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -12,10 +12,9 @@
     1.4  imports Main "~~/src/HOL/Library/While_Combinator"
     1.5  begin
     1.6  
     1.7 -types 
     1.8 -  'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 -  'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.10 -  'a sl     = "'a set \<times> 'a ord \<times> 'a binop"
    1.11 +type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.12 +type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.13 +type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
    1.14  
    1.15  consts
    1.16    "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"