Map.empty now qualified to avoid name clashes
authornipkow
Fri Jun 15 10:45:12 2018 +0200 (10 months ago)
changeset 6845041de07c7a0f3
parent 68449 6d0f1a5a16ea
child 68451 c34aa23a1fb6
Map.empty now qualified to avoid name clashes
NEWS
src/HOL/Library/RBT_Impl.thy
src/HOL/Map.thy
     1.1 --- a/NEWS	Thu Jun 14 17:50:23 2018 +0200
     1.2 +++ b/NEWS	Fri Jun 15 10:45:12 2018 +0200
     1.3 @@ -320,6 +320,8 @@
     1.4  
     1.5    - list comprehension syntax now supports tuple patterns in "pat <- xs"
     1.6  
     1.7 +* Theory Map: "empty" must now be qualified as "Map.empty".
     1.8 +
     1.9  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
    1.10  
    1.11  * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
     2.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Jun 14 17:50:23 2018 +0200
     2.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jun 15 10:45:12 2018 +0200
     2.3 @@ -166,7 +166,7 @@
     2.4  lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> rbt_lookup t k = None"
     2.5  by (induct t) auto
     2.6  
     2.7 -lemma rbt_lookup_Empty: "rbt_lookup Empty = empty"
     2.8 +lemma rbt_lookup_Empty: "rbt_lookup Empty = Map.empty"
     2.9  by (rule ext) simp
    2.10  
    2.11  end
     3.1 --- a/src/HOL/Map.thy	Thu Jun 14 17:50:23 2018 +0200
     3.2 +++ b/src/HOL/Map.thy	Fri Jun 15 10:45:12 2018 +0200
     3.3 @@ -826,4 +826,6 @@
     3.4    qed
     3.5  qed
     3.6  
     3.7 +hide_const (open) Map.empty
     3.8 +
     3.9  end