Mercurial Mercurial > repos > Old_HOL / 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.
IOA/example/Lemmas.thy
author nipkow
Fri, 02 Dec 1994 11:43:20 +0100
changeset 194 b93cc55cb7ab
parent 168 44ff2275d44f
permissions -rw-r--r--
small updates because datatype list is now used. In particular Nil -> []
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
168
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset 
     1
 
(*  Title:      HOL/IOA/example/Lemmas.thy
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset 
     2
 
    ID:         $Id$
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset 
     3
 
    Author:     Tobias Nipkow & Konrad Slind
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset 
     4
 
    Copyright   1994  TU Muenchen
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset 
     5
 












44ff2275d44f
Added headers and made various small mods.



nipkow


parents: 
156

diff
changeset




     6


Arithmetic lemmas













44ff2275d44f
Added headers and made various small mods.



nipkow


parents: 
156

diff
changeset




     7


*)













44ff2275d44f
Added headers and made various small mods.



nipkow


parents: 
156

diff
changeset




     8









156






fd1be45b64bf
added IOA to isabelle/HOL



clasohm


parents: 

diff
changeset




     9


Lemmas = Arith















Old_HOL