Hi Florian,
the simproc unit_eq in
http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78
rewrites anything of type unit to (), so there's no need to declare the definitions
introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def,
On 11.06.2014, at 2:56 pm, Thomas Sewell thomas.sew...@nicta.com.au wrote:
Gerwin will push the isabelle hypsubst change to the testboard now (assuming
he can remember how).
He could and did.
Cheers,
Gerwin
The information in this e-mail may be
On 11.06.2014 06:56, Thomas Sewell wrote:
OK, I've finished the needed adjustments the AFP proofs which were
affected by the hypsubst change.
The result is fairly encouraging: the AFP is *huge* and the diffstat
of the required changes is:
63 files changed, 134 insertions(+), 81 deletions(-)
On 11/06/2014 23:56, Florian Haftmann wrote:
Unfinished session(s): CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker,
CAVA_buildchain1, CAVA_buildchain3, Gabow_SCC, LTL_to_GBA,
MonoBoolTranAlgebra, Promela
I have a suspicion that the dropout in MonoBoolTranAlgebra is due to
