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)"
```