Re: [isabelle] Simplifier and linorder transitivity



On Thu, 7 Mar 2013, Ognjen Maric wrote:

   fun is_le_prem thm = (
       prop_of thm
               |> HOLogic.dest_Trueprop
               |> head_of
               |> equal less
   ) handle _ => false

Just note that "handle _ => ..." makes the ML program ill-defined, subject to the laws of phyisics instead of mathematics. See also the explanation in section 0.5 of the Isabelle/Isar Implementation manual http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf

After many years of practice, I am conditioned to watch out for such snags, which is why I've spotted it in your code without looking for anything in particular.


	Makarius





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