Email Gateway (Aug 18 2022 at 12:46): Email Gateway (Aug 18 2022 at 12:46):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
I am having a strange event when importing a theory. It processes
fine, then there seems to be some problem with registering it as
processed, namely ~2000 lines a MATCH warnings/errors. A partial trace
from a ProofGeneral session follows, but it does not appear to be
ProofGeneral specific as the warnings turn up in a build log as well.
\<^sync>ProofGeneral.inform_file_processed "/home/mahonyb/work/ver/REP/
HiVe_Isa08/mathKit/Equipotence.thy"; \<^sync>;
Enter MATCH
%a b c d e. e =?= ?P48 z
%a b. b =?= ?P23 z
%a b c. c =?= ?P22 z
%a b c. c =?= ?P21 z
%a b c. c =?= ?P20 z
%a b c. c =?= ?P19 z
%a b. b =?= ?P18 z
%a b. b =?= ?P17 z
%a b c. c =?= ?P16 z
%a b c. c =?= ?P15 z
%a b c. c =?= ?P14 z
%a b c. c =?= ?P13 z
%a b. b =?= ?P12 z
%a. a =?= ?P11 z
%a b c. c =?= ?P10 z
%a b c. c =?= ?P9 z
%a b c. c =?= ?P8 z
%a b c. c =?= ?P7 z
%a b. b =?= ?P6 z
%a. a =?= ?P5 z
Enter MATCH
etc etc etc
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Email Gateway (Aug 18 2022 at 12:46):From: Lawrence Paulson <lp15@cam.ac.uk>
Your problem is almost certainly caused by the postprocessing phase,
which makes the theorems you have just proved available to
sledgehammer. If you send me your theory file, I can try to identify
which theorem is to blame. As an emergency measure, you can execute
ML{ResAxioms.suppress_endtheory := true}
If you do not use sledgehammer, you can leave this setting as the
default.
Larry
Last updated: May 03 2024 at 08:18 UTC