Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2020-RC1: ML exception with unused_thms

view this post on Zulip Email Gateway (Aug 23 2022 at 08:39):

From: Mark Wassell <mpwassell@gmail.com>
Hello,

With the following

theory Unused imports Main begin

lemma mylem: assumes "A ∧ B" shows B using assms by auto

unused_thms

I get this exception in Isabelle 2020 RC1 but not in 2019.

CONTEXT
("No content for theory certificate Draft.Unused:79", [], [],
["??.HOL.Trueprop (??.HOL.conj ?A ?B) ⟹ ??.HOL.Trueprop ?B"],
NONE) raised (line 528 of "thm.ML")

Cheers

Mark

view this post on Zulip Email Gateway (Aug 23 2022 at 08:39):

From: Makarius <makarius@sketis.net>
Thank you for testing. I have changed it for the next release candidate here:
https://isabelle-dev.sketis.net/rISABELLEc983fd846c9

Makarius

Last updated: Nov 21 2024 at 12:39 UTC