# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID 559f4552880484877b7163d8cf62abf302db38db
# Parent  9bd8c16b6627162305206c16f5543efc5b0c141a
dropped former legacy input abbreviations

diff -r 9bd8c16b6627 -r 559f45528804 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Main.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -18,31 +18,6 @@
     GCD
 begin
 
-text \<open>Legacy\<close>
-
-context Inf
-begin
-
-abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
-
-end
-
-context Sup
-begin
-
-abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
-
-end
-
-abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
-  where "INTER \<equiv> INFIMUM"
-
-abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
-  where "UNION \<equiv> SUPREMUM"
-
-
 text \<open>Namespace cleanup\<close>
 
 hide_const (open)