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 wenzelm
Wed, 02 Aug 2000 19:40:14 +0200
changeset 9502 50ec59aff389
parent 9102 c7ba07e3bbe8
child 9771 54c6a2c6e569
permissions -rw-r--r--
adapted deriv;
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









9102






c7ba07e3bbe8
fixed deps;



wenzelm


parents: 
5261

diff
changeset




     9


ListOrder = Acc +








5261






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