--- a/src/HOL/MicroJava/DFA/Semilat.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Sat Apr 23 13:00:19 2011 +0200
@@ -12,10 +12,9 @@
imports Main "~~/src/HOL/Library/While_Combinator"
begin
-types
- 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
- 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
+type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
consts
"lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"