src/HOL/Library/FuncSet.thy
changeset 56777 9c3f0ae99532
parent 54417 dbb8ecfe1337
child 58606 9c66f7c541fb
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:48:59 2014 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:50:03 2014 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  abbreviation
     1.5    funcset :: "['a set, 'b set] => ('a => 'b) set"
     1.6      (infixr "->" 60) where
     1.7 -  "A -> B == Pi A (%_. B)"
     1.8 +  "A -> B \<equiv> Pi A (%_. B)"
     1.9  
    1.10  notation (xsymbols)
    1.11    funcset  (infixr "\<rightarrow>" 60)
    1.12 @@ -41,8 +41,8 @@
    1.13    "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.14  
    1.15  translations
    1.16 -  "PI x:A. B" == "CONST Pi A (%x. B)"
    1.17 -  "%x:A. f" == "CONST restrict (%x. f) A"
    1.18 +  "PI x:A. B" \<rightleftharpoons> "CONST Pi A (%x. B)"
    1.19 +  "%x:A. f" \<rightleftharpoons> "CONST restrict (%x. f) A"
    1.20  
    1.21  definition
    1.22    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
    1.23 @@ -352,7 +352,7 @@
    1.24  
    1.25  syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    1.26  
    1.27 -translations "PIE x:A. B" == "CONST Pi\<^sub>E A (%x. B)"
    1.28 +translations "PIE x:A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (%x. B)"
    1.29  
    1.30  abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60) where
    1.31    "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"