This looks like a regression.
Can you turn this into an issue on github please?
Michael
From: Waqar Ahmad via hol-info
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 3 July 2018 at 01:41
To: hol-info
Subject: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12
Hi a
Hi all,
I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12
Consider a proof goal
``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)``
e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));
(* In HOL-k10, the tactic results a desired behavior*)
?!m. ((m = n) \/ m < n) /\
