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



Thanks Florian.

Can you push this please?

@Makarius: Will this make it into Isabelle2016-1?

--
 Peter



On Fr, 2016-11-18 at 20:58 +0100, Florian Haftmann wrote:
> 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
> 




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