src/HOL/Tools/atp-inputs/full_helper1.dfg

--- a/src/HOL/Tools/atp-inputs/full_helper1.dfg	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_helper1.dfg	Wed Sep 20 13:56:39 2006 +0200
@@ -1,10 +1,21 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality for full-types
+%functional equality and extensionality for full-types
+
+clause(
+forall([A, X, Y],
+or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
+    equal(typeinfo(X,A),typeinfo(Y,A)))),
+a9 ).
+
+clause(
+forall([A, X, Y],
+or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
+    hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
+a10 ).
 
 clause(
 forall([A, B, F, G],
 or( not(equal(typeinfo(hAPP(typeinfo(F,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B),typeinfo(hAPP(typeinfo(G,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B))),
     equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B))))),
-a18 ).
-
+a11 ).
\ No newline at end of file