Do you see the same output in the example as per the Tutorial? If you have
∃x’. x = 0 ∨ x’ = 0
then I’d be very surprised if qexists_tac `0` failed.
Best wishes,
Michael
On 21 Mar 2022, at 03:47, Brian Milnes
mailto:briangmil...@gmail.com>> wrote:
Folks,
What is wrong with the Euclid exa
Folks,
What is wrong with the Euclid example?
Pg 30 of the tutorial?
The `0` won't parse and I get
> e (qexists_tac `0`);
OK..
Exception raised at Tactical.Q_TAC:
No parse for quotation
Exception-
HOL_ERR
{message = "No parse for quotation", origin_function = "Q_TAC",
origin_s
Dear all,
I am working with infinite summation and real derivatives in HOL Light. I
can write a theorem for the derivative of the finite summation as follows:
g `!f s. FINITE s /\ (!a. a IN s ==> (f a has_real_derivative f' a)
(atreal t))
==> real_derivative (\x. sum s (\a. f a x)) t = sum
Title: Bill McCune PhD Award in Automated Reasoning, Call for Nominations
***
Automated Reasoning is the area of Computer Science dedicated to applying
reasoning in the form of logic to computing systems. The Bill McCune PhD Award
in Automat
