[isabelle] Opaque ascription for SML code generation



Hi,

Is there a way to make the SML code generator use opaque ascription "structure Foo :> FOO = struct ... end" rather than transparent ascription "structure Foo : FOO = struct ... end"?

OCaml does not have transparent ascription so perhaps the default for SML should be opaque ascription.

Thanks,

Jørgen




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