src/HOL/Library/FuncSet.thy
changeset 67013 335a7dce7cb3
parent 67006 b1278ed3cd46
     1.1 --- a/src/HOL/Library/FuncSet.thy	Sun Nov 05 16:57:03 2017 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Nov 05 17:45:17 2017 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  theory FuncSet
     1.5    imports Main
     1.6    abbrevs PiE = "Pi\<^sub>E"
     1.7 -    PIE = "\<Pi>\<^sub>E"
     1.8 +    and PIE = "\<Pi>\<^sub>E"
     1.9  begin
    1.10  
    1.11  definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"