dropped former legacy input abbreviations
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (4 weeks ago)
changeset 70336559f45528804
parent 70335 9bd8c16b6627
child 70337 48609a6af1a0
dropped former legacy input abbreviations
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Main.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -18,31 +18,6 @@
     1.4      GCD
     1.5  begin
     1.6  
     1.7 -text \<open>Legacy\<close>
     1.8 -
     1.9 -context Inf
    1.10 -begin
    1.11 -
    1.12 -abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.13 -  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
    1.14 -
    1.15 -end
    1.16 -
    1.17 -context Sup
    1.18 -begin
    1.19 -
    1.20 -abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.21 -  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
    1.22 -
    1.23 -end
    1.24 -
    1.25 -abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    1.26 -  where "INTER \<equiv> INFIMUM"
    1.27 -
    1.28 -abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    1.29 -  where "UNION \<equiv> SUPREMUM"
    1.30 -
    1.31 -
    1.32  text \<open>Namespace cleanup\<close>
    1.33  
    1.34  hide_const (open)