src/HOL/Library/FuncSet.thy
changeset 64917 5db5b8cf6dc6
parent 64910 6108dddad9f0
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:24 2017 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 16:11:47 2017 +0100
     1.3 @@ -22,9 +22,6 @@
     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 (ASCII)
     1.8 -  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
     1.9 -  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.10  syntax
    1.11    "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.12    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.13 @@ -349,8 +346,6 @@
    1.14  
    1.15  abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
    1.16  
    1.17 -syntax (ASCII)
    1.18 -  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
    1.19  syntax
    1.20    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    1.21  translations