# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257532989 -3600
# Node ID 893a8e789d7f9c288a80c9b9f37595e3b41f04f2
# Parent  df72870f38fb33840be8a7c966739837ed3f5013
permutation lifting works now also

diff -r df72870f38fb -r 893a8e789d7f LFex.thy
--- a/LFex.thy	Fri Nov 06 19:26:32 2009 +0100
+++ b/LFex.thy	Fri Nov 06 19:43:09 2009 +0100
@@ -159,7 +159,6 @@
 thm FV_trm_def
 
 (* FIXME: does not work yet *)
-(*
 overloading
     perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"   (unchecked)
     perm_ty   \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"       (unchecked)
@@ -169,7 +168,19 @@
 quotient_def 
   perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> KIND \<Rightarrow> KIND)"
+  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
+
+quotient_def 
+  perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
+where
+  "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
+
+quotient_def 
+  perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+where
+  "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
+
 end
-*)
+
 
+