On Wed, 4 Aug 2010, Thomas Sewell wrote:
I was about to have another attempt at speeding up a tactic we
implemented for L4.verified using net-matching. In reading Pure/net.ML I
spotted the comment "Requires operands to be beta-eta-normal." In
rereading the existing biresolution_from_nets_tac c
On Mon, 2 Aug 2010, Walther Neuper wrote:
Trying to build the project from the Isabelle2009-2 distribution (cloned
from the hg repository) in the NetBeans IDE we got stuck:
(1) a screenshot of the NetBeans project is attached
(2) builds fail with the message:
/usr/local/isabisac/src/Tools/jEd
This sort of thing is well-known but very rare these days. I guess it could
trap an unwary user. It just isn't easy to fix, given the old strategy of using
assumptions, discarding them, and repeating.
Larry
On 5 Aug 2010, at 06:33, John Matthews wrote:
> Was it ever resolved whether auto should
Hi Lars,
You are mis-reading the schematic goal below:
lemma
"ALL (x::nat). x = y ==> False"
apply (erule allE)
After this step, the subgoal "?x = y ==> False" remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: "?x = y ==> False"
sorry
lemma "False" by (auto int
On 05.08.2010 09:24, Lars Noschinski wrote:
On 05.08.2010 07:33, John Matthews wrote:
lemma
"ALL (x::nat). x = y ==> False"
apply (erule allE)
After this step, the subgoal "?x = y ==> False" remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: "?x = y ==> False"
Forgo
On 05.08.2010 07:33, John Matthews wrote:
lemma
"ALL (x::nat). x = y ==> False"
apply (erule allE)
After this step, the subgoal "?x = y ==> False" remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: "?x = y ==> False"
sorry
lemma "False" by (auto intro: foo[of 1 1,
