Hi Brian, http://isabelle.in.tum.de/repos/isabelle/diff/001d1aad99de/src/HOL/Nat_Numeral.thy adds power_2_eq_1_iff as [simp], which breaks Fermat_3_4 in AFP. Although this can be repaired easily, I have the feeling that this rule which, if applied to an assumption, produces disjunctive proofs, should not be [simp] by default.
Cheers,
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
