Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/atp-inputs/u_helper1.dfg
author paulson
Thu, 21 Sep 2006 17:33:11 +0200
changeset 20661 46832fee1215
parent 20645 5e28b8f2cb52
permissions -rw-r--r--
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19717
2742cec21579 Helper files in DFG format.
mengj
parents:
diff changeset 
     1
 
%ID: $Id$
2742cec21579 Helper files in DFG format.
mengj
parents:
diff changeset 
     2
 
%Author: Jia Meng, NICTA
20645
5e28b8f2cb52 Moved the functional equality axioms to helper1 files.
mengj
parents: 19717
diff changeset 
     3
 
%functional equality and extensionality, untyped
5e28b8f2cb52 Moved the functional equality axioms to helper1 files.
mengj
parents: 19717
diff changeset 
     4
 












5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




     5


clause(













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




     6


forall([X, Y],













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




     7


or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




     8


    equal(X,Y))),













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




     9


a9 ).













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    10














5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    11


clause(













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    12


forall([X, Y],













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    13


or( not(equal(X,Y)),













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    14


    hBOOL(hAPP(hAPP(fequal,X),Y)))),













5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    15


a10 ).








19717






2742cec21579
Helper files in DFG format.



mengj


parents: 

diff
changeset




    16














2742cec21579
Helper files in DFG format.



mengj


parents: 

diff
changeset




    17


clause(













2742cec21579
Helper files in DFG format.



mengj


parents: 

diff
changeset




    18


forall([F, G],













2742cec21579
Helper files in DFG format.



mengj


parents: 

diff
changeset




    19


or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G)))),













2742cec21579
Helper files in DFG format.



mengj


parents: 

diff
changeset




    20


    equal(F,G))),








20645






5e28b8f2cb52
Moved the functional equality axioms to helper1 files.



mengj


parents: 
19717

diff
changeset




    21


a11 ).














isabelle