Re: [isabelle] A way to write nested theories in a theory file?

Le Fri, 08 Feb 2013 04:24:23 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at> a écrit:

I think this simple pattern can fulfil the needs:

     local L‑n context L‑n
       (* Isar samples goes here *)

Just have to not forget to properly manage all the “‑n” everywhere.

Sorry, typo. Add “begin”:

    local L‑n context L‑n begin
      (* Isar samples goes here *)

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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