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 wrote:
>
> On Thu, 30 Oct 2014, Florian Haftmann wrote:
>
> Isabell
>
> 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 abo
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 usa
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:
* Makarius [2014-11-03 10:30 +0100]:
> On Mon, 3 Nov 2014, Timothy Bourke wrote:
>
> >* Makarius [2014-11-02 20:24 +0100]:
> >>*** Document preparation ***
> >>
> >>* Document headings work uniformly via the commands 'chapter',
> >>'section', 'subsection', 'subsubsection' -- in any context, even
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius [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 y
On Mon, 3 Nov 2014, Peter Lammich wrote:
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 unifi
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, ...,
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
* Makarius [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 a
10 matches
Mail list logo
