I’m glad to have your support. It’s just possible that I might ask your help in getting some things working in the AFP.
Larry > On 10 Nov 2015, at 17:53, Manuel Eberl <ebe...@in.tum.de> wrote: > > This is very nice to hear. ‘real’ has plagued me for some time now and I am > glad to see it gone. > > Thanks for the good work! > > > On 10/11/15 17:45, Lawrence Paulson wrote: >> The first phase of this project is finished: the function “real” now has the >> monomorphic type nat => real and is simply an abbreviation for the generic >> function, of_nat. In addition, the function “real_of_int” abbreviates the >> generic function of_int. >> >> It took about a week to convert all the theories in the main Isabelle/HOL >> directory. Most of them needed little or no attention, the big exceptions >> being Probability (which frequently used “real” with the type ereal => real) >> and Decision_Procs, which contained many thousands of instances of “real” on >> integers and floats. >> >> The main priority at the moment is to fix the decision procedure mir, which >> isn’t working but appears to be entirely unused. Then there is still a lot >> of cleaning up to do, especially in Real.thy and its ancestors. Two or three >> dozen theorems existed in duplicate forms, with versions for “real” separate >> from versions for the other coercions; occasionally these variants were >> named systematically, but often their names were unrelated from the >> originals, and the names of variables in the theorems were almost always >> different. The simplification status of the two variants generally differed >> as well. Thus the behaviour of the simplifier on a formula depended on which >> coercion had been used, and in 150 cases, the simplification itself included >> the mapping of one coercion to another (there were two equivalent theorems >> for doing this). >> >> Innumerable type constraints have now become redundant (things such as >> real_of_int (i::int)), but I intend to leave them as they are. I have a lot >> of AFP entries to fix. >> >> Larry >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
