Can someone have a look at what is going wrong in Locally-Nameless-Sigma?
It looks like a bug in the datatype package is being triggered:
*** Stale theory encountered:
*** {Pure, Code_Generator, HOL, Orderings, Groups, Lattices, Set,
*** Complete_Lattice, Typedef, Inductive, Fun, Product_Type, Rings, Fields,
*** Sum_Type, Nat, Datatype, Complete_Partial_Order, Option, Power,
*** Finite_Set, Relation, Predicate, Transitive_Closure, Partial_Function,
*** Wellfounded, Meson, FunDef, Extraction, Metis, Plain, Big_Operators,
*** Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides,
*** Numeral_Simprocs, Semiring_Normalization, Groebner_Basis, SetInterval,
*** Hilbert_Choice, Presburger, Recdef, Code_Numeral, Quotient, ATP, List,
*** String, Typerep, Map, Random, Code_Evaluation, Enum, Lazy_Sequence,
*** Quickcheck, DSequence, Random_Sequence, New_DSequence,
*** New_Random_Sequence, Record, SMT, Sledgehammer, Refute, SAT,
*** Predicate_Compile, Quickcheck_Exhaustive, Nitpick, Main, ListPre, FMap,
*** Sigma:162, #, !}
*** At command "datatype" (line 80 of
"/home/kleing/afp/devel/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy")
Cheers,
Gerwin
Begin forwarded message:
From: Gerwin Klein<kle...@ertos.nicta.com.au>
Date: 8 April 2011 6:21:49 AM AEST
To:<kle...@cse.unsw.edu.au>
Subject: status (AFP)
The status of the following AFP entries changed or remains FAIL:
[Locally-Nameless-Sigma] is still on FAIL.
Full entry status at http://afp.sourceforge.net/status.shtml
AFP version: development -- hg id 29a8783494d0
Isabelle version: devel -- hg id 7d08265f181d
Test ended on: lemma, Fri Apr 8 06:21:49 EST 2011.
Have a nice day,
isatest
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
