src/HOL/UNITY/Extend.thy
changeset 61943 7fba644ed827
parent 61941 31f2105521ee
child 61952 546958347e05
     1.1 --- a/src/HOL/UNITY/Extend.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  definition
     1.5    (*MOVE to Relation.thy?*)
     1.6    Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
     1.7 -  where "Restrict A r = r \<inter> (A <*> UNIV)"
     1.8 +  where "Restrict A r = r \<inter> (A \<times> UNIV)"
     1.9  
    1.10  definition
    1.11    good_map :: "['a*'b => 'c] => bool"
    1.12 @@ -23,7 +23,7 @@
    1.13    
    1.14  definition
    1.15    extend_set :: "['a*'b => 'c, 'a set] => 'c set"
    1.16 -  where "extend_set h A = h ` (A <*> UNIV)"
    1.17 +  where "extend_set h A = h ` (A \<times> UNIV)"
    1.18  
    1.19  definition
    1.20    project_set :: "['a*'b => 'c, 'c set] => 'a set"