On Wed, Aug 17, 2011 at 11:51 AM, Florian Haftmann <[email protected]> wrote: > HOLCF-Library FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/c478cd500dc4
> HOL-Bali FAILED > HOL-Decision_Procs FAILED > HOL-Induct FAILED > HOL-Subst FAILED > HOL-NanoJava FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/b922e91dd1d9 > HOL-Multivariate_Analysis FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/7784fa3232ce > HOL-IMP FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/e44f465c00a1 > HOL-ex FAILED I looked into this, and as far as I can tell, there are two theories left that have problems. First, ex/Refute_Examples.thy raises exception REFUTE on line 113: lemma "distinct [a,b]" refute Second, ex/set.thy freezes on the "force" methods from lines 180 and 197: lemma "a < b & b < (c::int) ==> EX A. a ~: A & b : A & c ~: A" by force lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)" by (simp add: abs_if, force) > Possible showstoppers: > src/HOL/Library/Cset.thy This one requires a design decision: What should the type of the "member" function be? It could be either "'a Cset.set => 'a set" or "'a Cset.set => 'a => bool". Similarly, "Set" could be either "'a set => 'a Cset.set" or "('a => bool) => 'a Cset.set". > src/HOL/Nominal/Nominal.thy I have done some playing around with this, but the required changes include class instances for the "set" type, and so they cannot be merged back into the main distribution. > A glimpse at the AFP: > thys/Shivers-CFA/ExCFSV.thy > thys/Shivers-CFA/HOLCFUtils.thy Updating this one will require class instances for the "set" type; the changes are not backward compatible. > thys/Presburger-Automata/Presburger_Automata.thy > thys/Presburger-Automata/DFS.thy Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/b8be79162da4 > thys/SIFPL/VS.thy > thys/SIFPL/VS_OBJ.thy > thys/SIFPL/HuntSands.thy Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/8d44eafb4517 - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
