Re: [isabelle-dev] Isabelle (proof assistant) - Wikipedia, the free encyclopedia

. 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

[isabelle-dev] Feature suggestion: apply (meth[1!])

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Ã

Re: [isabelle-dev] Feature suggestion: apply (meth[1!])

. 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

Re: [isabelle-dev] Code export to Haskell and lower-case theory names

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

Re: [isabelle-dev] Code export to Haskell and lower-case theory names

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

Re: [isabelle-dev] Code export to Haskell and lower-case theory names

-- 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

Re: [isabelle-dev] Interpretation in arbitrary targets.

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

Re: [isabelle-dev] Proper AFP history on the web

/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

Re: [isabelle-dev] Orphaned theory in AFP

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

Re: [isabelle-dev] Isabelle World Map

-- 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

Re: [isabelle-dev] NEWS: method facts

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

Re: [isabelle-dev] NEWS: method facts

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›)  ...