Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main



Hi all,

> I think I made some changes to the imports during my overhaul of rings.
> It had something to do with pending sort hypotheses. In retrospect, a
> more ad-hoc solution may have been the better choice considering these
> complaints now.

the restoration of the previous situation is trivial:

> diff -r 0da35bf3e6cf src/HOL/Word/Bool_List_Representation.thy
> --- a/src/HOL/Word/Bool_List_Representation.thy	Thu Nov 17 16:32:53 2016 +0100
> +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Nov 18 20:56:02 2016 +0100
> @@ -9,7 +9,7 @@
>  section "Bool lists and integers"
>  
>  theory Bool_List_Representation
> -imports Complex_Main Bits_Int
> +imports Main Bits_Int
>  begin
>  
>  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
> @@ -1106,7 +1106,7 @@
>    apply (case_tac m)
>    apply simp
>    apply (case_tac "m <= n")
> -   apply auto
> +   apply (auto simp add: div_add_self2)
>    done
>  
>  lemma bin_rsplit_len: 

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.