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/Lambda/ListOrder.thy
author paulson
Thu, 01 Oct 1998 18:30:05 +0200
changeset 5601 b6456ccd9e3e
parent 5261 ce3c25c8a694
child 9102 c7ba07e3bbe8
permissions -rw-r--r--
revised for new treatment of integers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset 
     1
 
(*  Title:      HOL/Lambda/ListOrder.thy
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset 
     2
 
    ID:         $Id$
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset 
     3
 
    Author:     Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset 
     4
 
    Copyright   1998 TU Muenchen
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset 
     5
 












ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




     6


Lifting an order to lists of elements, relating exactly one element













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




     7


*)













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




     8














ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




     9


ListOrder = List + Acc +













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    10














ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    11


constdefs













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    12


 step1 :: "('a * 'a)set => ('a list * 'a list)set"













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    13


"step1 r ==













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    14


   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"













ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    15














ce3c25c8a694
First steps towards termination of simply typed terms.



nipkow


parents: 

diff
changeset




    16


end















isabelle