src/HOL/Library/FuncSet.thy
changeset 61955 e96292f32c3c
parent 61585 a9599d3d7610
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -20,10 +20,10 @@
     1.4  abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
     1.5    where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
     1.6  
     1.7 -syntax
     1.8 +syntax (ASCII)
     1.9    "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
    1.10    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.11 -syntax (xsymbols)
    1.12 +syntax
    1.13    "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.14    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.15  translations
    1.16 @@ -347,11 +347,12 @@
    1.17  
    1.18  abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
    1.19  
    1.20 -syntax
    1.21 +syntax (ASCII)
    1.22    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
    1.23 -syntax (xsymbols)
    1.24 +syntax
    1.25    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    1.26 -translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
    1.27 +translations
    1.28 +  "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
    1.29  
    1.30  abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
    1.31    where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"