You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on May 23, 2023. It is now read-only.
Somewhat similar to #5, though not sure whether due to the same cause. Isabelle rejects the proof of the theorem in module test4, but accepts the proof for the same theorem in module test5.
--------------------------------- MODULEtest4 ---------------------------------
(* A proof is found, but Isabelle rejects it. *)Support(R)=={p[1]:p\inDOMAINR}\cup{p[2]:p\inDOMAINR}THEOREMASSUMENEWFoo,\Ax\inSupport(Foo):Foo[x,x]PROVELETR==Support(Foo)Bar==[t\inR\XR|->Foo[t[1],t[2]]]IN\Ax\inSupport(Bar):Bar[x,x]<1>DEFINER==Support(Foo)Bar==[t\inR\XR|->Foo[t[1],t[2]]]Q==Support(Bar)<1>1. Q=ROMITTED(* Can be proved, but omitted here for brevity. *)<1>QEDBY<1>1
================================================================================
Somewhat similar to #5, though not sure whether due to the same cause. Isabelle rejects the proof of the theorem in module
test4
, but accepts the proof for the same theorem in moduletest5
.In this case
isabelle.log
readsand line 124 in
test4.thy
is:In contrast:
In module
test5
, if<1> HIDE DEF Bar
is removed, then Isabelle rejects the proof of step<2>3. << x, x >> \in R \X R
.The text was updated successfully, but these errors were encountered: