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/Vimage.thy
author paulson
Tue, 08 Sep 1998 15:17:11 +0200
changeset 5434 9b4bed3f394c
parent 4648 f04da668581c
child 7515 0c05469cad57
permissions -rw-r--r--
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4648
f04da668581c New theory of the inverse image of a function
paulson
parents:
diff changeset 
     1
 
Vimage = Set +
f04da668581c New theory of the inverse image of a function
paulson
parents:
diff changeset 
     2
 












f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     3


consts













f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     4


  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)













f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     5














f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     6


defs













f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     7


  vimage_def     "f-``B           == {x. f(x) : B}"













f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     8














f04da668581c
New theory of the inverse image of a function



paulson


parents: 

diff
changeset




     9


end















isabelle