src/HOL/Relation.thy
changeset 19656 09be06943252
parent 19363 667b5ea637dd
child 20716 a6686a8e1b68
     1.1 --- a/src/HOL/Relation.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -12,13 +12,14 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
    1.10    "r^-1 == {(y, x). (x, y) : r}"
    1.11 -syntax (xsymbols)
    1.12 -  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\<inverse>)" [1000] 999)
    1.13  
    1.14 -constdefs
    1.15 +const_syntax (xsymbols)
    1.16 +  converse  ("(_\<inverse>)" [1000] 999)
    1.17 +
    1.18 +definition
    1.19    rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
    1.20    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
    1.21