[isabelle] programming with locales



Hello all,

I would like to emulate the following locale definition

----------------------------------------------------------------------
locale globals = 
  fixes 
    x_address :: nat
  assumes
    x_nzero:    "x_address ~= 0" and
    x_aligned:  "4 dvd x_address"
----------------------------------------------------------------------

at the ML level, and then go onto make some definitions within the
locale (i.e., the sort of thing you would write with defines clauses),
but for which I already have ML code using add_consts_defs_i.

What should my ML code look like?

Many thanks,
Michael.







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