[isabelle] Formal comments within inner syntax

Dear all,

I wonder whether there is any way in Isabelle to include formal, checked comments within inner syntax in Isabelle. In Haskell, for example, one frequently sees function signatures of the following layout:

  :: [a]       -- meaning of first parameter
  -> Integer   -- meaning of second parameter
  -> (a, [a])  -- description of results

I find this format very convenient to document functions with a large number of parameters. However, in Isabelle, I have not yet found a satisfactory solution. The following is already close to the above, however it relies on comments within inner syntax. Hence, the documentation is not formally checked and I cannot use antiquotations and all the other conveniences from formal text blocks.

definition my_fun
  :: "'a list         (* meaning of first parameter *)
   => int             (* meaning of second parameter *)
   => ('a, 'a list)"  (* description of results *)
where ...

Can such comments be made such that they are checked formally? Or does any of you have other convenient ways of documenting parameters and results of functions?


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