Re: [isabelle-dev] NEWS: uniform document heading commands
* Makarius makar...@sketis.net [2014-11-02 20:24 +0100]: *** Document preparation *** * Document headings work uniformly via the commands 'chapter', 'section', 'subsection', 'subsubsection' -- in any context, even before the initial 'theory' command. Very nice. Thank you. Would it also be reasonable to allow 'text' before an initial 'theory' ? Tim. signature.asc Description: Digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] How to activate/de-activate unifier-trace from ML-level
Hi List, I have a tactic that has a debug-mode. In debug-mode, it shall output unification trace for certain (but not all) rule applications. How to write a tactic resolve_with_tracing: thm list - int - tactic that behaves like resolve_tac, but outputs unification trace? Best, Peter p.s. Not sure whether this belongs to user or devel, but the reason for my message is http://sourceforge.net/p/afp/code/ci/7189f7ffd73e17c2395eb552c89004f5b8e0453e/ which seems to be related to tty-mode elimination that is currently going on in dev-version. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.
On Thu, 30 Oct 2014, Florian Haftmann wrote:
Isabelle/ML has antiquotations as some kind of macro language. It can
do certain things better than the C preprocessor, although one always
needs to be careful to stay within reason.
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
Maybe even this as well?
@{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn)
That might be occasionally useful to map field 1, or 2, or 3 of a triple:
@{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}. The existing combinators apfst,
apsnd fit into the same scheme.
Both have there uses. I am not sure whether »ap« is the right name.
»apfst« and »apsnd« are of course old-standing items, but when something
new enters the stage further thoughts should be spent. Must confess I
have no better proposal at hand. Or maybe »apply«?.
Larry, you have introduced the pairself name some decades ago. How do
you feel about it being called ap2 or apply2?
Makarius
http://stop-ttip.org 777,356 people so far
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
On Mon, 3 Nov 2014, Timothy Bourke wrote: * Makarius makar...@sketis.net [2014-11-02 20:24 +0100]: *** Document preparation *** * Document headings work uniformly via the commands 'chapter', 'section', 'subsection', 'subsubsection' -- in any context, even before the initial 'theory' command. Very nice. Thank you. Would it also be reasonable to allow 'text' before an initial 'theory' ? I have asked myself that yesterday, when updating some AFP entries in that respect. The canonical question: Is such a feature really needed? So far the standard way is to say 'theory' first, before writing longer paragraphs of text. The concept of Isabelle document preparation is to write in a formal context (which is required for antiquotations), but before the theory start it is undefined. Makarius http://stop-ttip.org 777,460 people so far ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
* Makarius makar...@sketis.net [2014-11-03 10:30 +0100]:
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius makar...@sketis.net [2014-11-02 20:24 +0100]:
*** Document preparation ***
* Document headings work uniformly via the commands 'chapter',
'section', 'subsection', 'subsubsection' -- in any context, even
before the initial 'theory' command.
Very nice. Thank you.
Would it also be reasonable to allow 'text' before an initial 'theory' ?
I have asked myself that yesterday, when updating some AFP entries in that
respect.
The canonical question: Is such a feature really needed?
So far the standard way is to say 'theory' first, before writing longer
paragraphs of text. The concept of Isabelle document preparation is to
write in a formal context (which is required for antiquotations), but before
the theory start it is undefined.
I was thinking of the case where one wants to break up a set of
theories into chapters while still keeping each theory within its own
section.
The first theory in a new chapter could now start:
chapter Theories A-D
section Theory A
theory A imports Main begin ... end
In this case, 'text' would be useful for writing introductory
paragraphs between 'chapter' and 'section'.
But, maybe it is better to dedicate a theory file to new chapters :
chapter Theories A-D
theory %invisible begin
text {* ... *}
end %invisible
And then a top-level 'text' is not needed.
Does anyone else had similar experiences with structuring proof
documents?
Tim.
signature.asc
Description: Digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
Am Montag, den 03.11.2014, 10:30 +0100 schrieb Makarius: On Mon, 3 Nov 2014, Timothy Bourke wrote: Would it also be reasonable to allow 'text' before an initial 'theory' ? I have asked myself that yesterday, when updating some AFP entries in that respect. The canonical question: Is such a feature really needed? So far the standard way is to say 'theory' first, before writing longer paragraphs of text. The concept of Isabelle document preparation is to write in a formal context (which is required for antiquotations), but before the theory start it is undefined. In most cases I want to write a small (informal) introduction. But then the theory ... imports ... begin command looks out of place in the generated document and I hide it using (**) (**). So having a way to write an abstract / or an informal introduction would be nice. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Experiments in best-first-search rewriter
On Sun, 2 Nov 2014, Bohua Zhan wrote: Two examples are given at the end: the first refers to the permutation example in section 6.4 of the new Isabelle Cookbook manual, rewriting: Note that the Isabelle Cookbok is not really new. It is useful to get started in some areas of Isabelle/ML usage, but it also contains many things that are old, or outright misleading. You need to take other information into account as well, and develop a sense of (un)reliability of certain information. The official implementation manual is the main starting point for using Isabelle/ML. Using Isabelle/ML is not yet an Isabelle development activity, so it can be discussed on isabelle-users -- unless you want to propose concrete changes to ongoing repository versions. Makarius http://stop-ttip.org 777,535 people so far ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
You can contribute indirectly to important reforms that are in the pipeline for a long time by keeping your sources in a more up-to-date state. As you said, there seems to be no other way of achieving what I required. I realized that, added a comment (*Argh!*) expressing my disgust about it, but at the end had to implement the hack in order to get the desired behaviour. Now you just removed the desired behaviour, not having a solution how to get it back ... fortunately, in this particular case, it is not essential, as this thing was inside some rarely used debugging tool. -- Peter Makarius http://stop-ttip.org 777,443 people so far ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.
I have to admit: although I distinctly remember the name pairself, I can’t
imagine what I could have been thinking when I chose this name. Your
suggestions make a lot more sense.
Larry
On 3 Nov 2014, at 09:08, Makarius makar...@sketis.net wrote:
On Thu, 30 Oct 2014, Florian Haftmann wrote:
Isabelle/ML has antiquotations as some kind of macro language. It can
do certain things better than the C preprocessor, although one always
needs to be careful to stay within reason.
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
Maybe even this as well?
@{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn)
That might be occasionally useful to map field 1, or 2, or 3 of a triple:
@{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}. The existing combinators apfst,
apsnd fit into the same scheme.
Both have there uses. I am not sure whether »ap« is the right name.
»apfst« and »apsnd« are of course old-standing items, but when something
new enters the stage further thoughts should be spent. Must confess I
have no better proposal at hand. Or maybe »apply«?.
Larry, you have introduced the pairself name some decades ago. How do you
feel about it being called ap2 or apply2?
Makarius
http://stop-ttip.org 777,356 people so far
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
