[isabelle] Opaque ascription for SML code generation


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.



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