http://isabelle.in.tum.de/reports/Isabelle/rev/8e0a1d0a41ff
This quotation is not very fair towards the Egyptian pyramids. It is
ignorant of contemporary historians' suppositions that »just« a few
thousand (personally free) workers had been working on a single pyramid,
does not justice to the log
Totally agree. Considering the tools they had available, they are
geniuses in my book. But there *is* a parallel with the workers who
build the pyramids. Although free, their skeletal remains clearly
show a life of hard labour and misery. Wished Isabelle developers
somehow had moved on from that
Hi all,
when Isabelle packages (in the widest sense) provide an interface to the
user, the following pattern is common practice:
> fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
> let
> val x_1 = prep_1 ctxt raw_x_1;
> …
> val x_n = prep_n ctxt raw_x_n;
> in
> ctxt
>
