# Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions

```Hi Makarius, hi all,

```
@All: Let me slowly resume the discussion of your feedback about our formalisation. The earlier feedback sent by others (thanks once more!) is not forgotten, I will get back to this next week, but the points in this mail are good for me to start with, as they don't require me to learn a lot of new things.
```
2012-11-16 22:49 Makarius:
```
```Since Christoph is also a CICM person, I would like to point out the MKM
2008 paper by myself and Stefan Berghofer on "Logic-free reasoning in
Isabelle/Isar".  It shows how to deflate your theories by a significant
factor, by removing unnecessary fluff.
```
```
Thanks for the pointer!

```
```(Informal people sometimes think
they are doing formal logic when writing a lot of logical connectives
around there meterial, but this is not the real point of it.)
```
```
```
Well, I actually didn't try to be as "formal" as possible, but I did not yet know how to do it right. In several lemmas I started with a simpler statement, e.g. just the right side of an implication, and put the left side into "assumes" declarations, but then I wasn't able to reuse these assumptions in the proof as expected. In the cumbersome way I ended up doing it I got the work done at least – but of course I'll be excited to learn about the nicer way of doing it, and how to avoid such pitfalls as I mentioned.
```
```
```Can you write your sources with 80 char per line, or 100 maximum?  These
exceedingly long lines are hard to read.  The physicial parameters of
cinema displays have changed a lot recently, but not the parameters of
the human brain.
```
```
```
OK, I will try; it should be possible to introduce line breaks where it semantically makes sense.
```
But actually I'd like to blame half of the problem on this:

```
```jEdit is not very good at soft line-breaks,
```
```
```
Not having much previous jEdit experience I simply had hoped that a modern editor would be good at that (even recent versions of dinosaurs such as Emacs are), and somehow denied that it didn't work so well after all.
```
End of rant; I don't want to start an editor war here.

```
```and it is better to layout
your formal sources explicitly yourself.  (The jEdit indentation
facilities still need to be activated for Isar sources, like I did many
years ago for Proof General / Emacs.)
```
```
```
Let me report a problem related to that: I tried at least to enable auto-indentation, so that any new line would be indented as much as the previous line. But with that I found that Isabelle didn't pick up the changes I made. (This is roughly what I remember from trying it a few weeks ago; if you'd like me to do some experiments and give a more detailed report, I'm happy to do so.)
```
Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

```

• Follow-Ups:
• References:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.