om the local variant to the corresponding context
specification command”.
This would allow me to write (applying the usual rules of the English
grammer):
lemma foo:
assumes "inductive_predicate x"
thuses "something_about x"
proof(use assms in ‹induction x›)
...
quot;
shows "something_about x"
p
roof(use assms in ‹induction x›)
...
qed
or is the need for method nesting no better than the extra using assms?
Thanks,
Joachim
--
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.i
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
it.
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
___
isabelle-dev mailing list
isabelle-...@in.tum.de
/p/afp/code/ci/908304753f7d30177997524427d78029ea77a331/
that cleanly shows all changes of that commit. You can manually shorten
it to
http://sourceforge.net/p/afp/code/ci/908304
and it still works.
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
looking forward to Isabelle 2013-2 (or 2014).
So thanks in advance from my side!
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
to choose his
naming, even if it deviate from what others use (she might have reasons
for that).
Greetings and happy easter to those who care,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description
Hi,
Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman:
On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner breit...@kit.edu wrote:
Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
This has got nothing to do with Isabelle's informal conventions but is
all about
. showing the current goal.
It is a bit verbose and does not work inside a (...)+ nesting, so I’d
still like the [!] or a similar method-level syntax, but at least it
works without modifying the prover.
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
to §6.3.1 of the reference
manual.
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
BinÀrdateien Isabelle2013/heaps/polyml-5.5.0_x86-linux/HOL and Isabelle2013-hacked/heaps/polyml-5.5.0_x86-linux/HOL sind verschieden.
BinÃ
. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
12 matches
Mail list logo