# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264510436 -3600
# Node ID 2c72447cdc0c6a7590bff4d4cd96524c103de907
# Parent  a792bfc1be2b75112e27a5fa309e45dcec4e3f8c
A triple is still ok.

diff -r a792bfc1be2b -r 2c72447cdc0c Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 13:38:42 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:53:56 2010 +0100
@@ -391,4 +391,11 @@
 apply(lifting test2)
 done
 
+lemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
+apply(lifting test3)
+done
+
 end