Email Gateway (Aug 22 2022 at 09:25): Email Gateway (Aug 22 2022 at 09:25):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
one week after Isabelle2015-RC1 there is now Isabelle2015-RC2:
http://isabelle.in.tum.de/website-Isabelle2015-RC2
Changes can be inspected here:
https://bitbucket.org/isabelle_project/isabelle-release/commits
With ever increasing size and complexity of the system and its many add-on
tools, it is important to take testing of release candidates seriously. So
far there were only minor issues, which indicates that really tough
testing has not happened yet.
The main forum for discussion is here on isabelle-users, but it is also
possible to contact the person who is responsible for particular Isabelle
tools via private mail -- better than keeping potential problems private.
When reporting problems, the subject line should be changed to something
meaningful.
Makarius
Email Gateway (Aug 22 2022 at 10:03):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I guess there are some superfluous lemmas in 2015-RC2 in Main:
theory Scratch
imports Main
begin
lemma "x = x"
Auto solve_direct: The current goal can be solved directly with
BNF_Composition.DEADID.map_ident: ?t = ?t
BNF_Composition.DEADID.rel_refl: ?x = ?x
Basic_BNF_LFPs.xtor_rel: ?R (Basic_BNF_LFPs.xtor ?x)
(Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y
Basic_BNF_LFPs.xtor_set: ?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x
HOL.refl: ?t = ?t
Cheers,
Cornelius
Email Gateway (Aug 22 2022 at 10:04):From: Larry Paulson <lp15@cam.ac.uk>
This is more an indication of the flexibility of Isabelle’s inference mechanisms that you can solve the goal
x = x
in one single step by applying the rule
?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x
or
?R (Basic_BNF_LFPs.xtor ?x) (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y .
I’m sure that these theorems, in the form given, serve some useful purpose.
Larry Paulson
Last updated: Apr 16 2024 at 08:18 UTC