Hi Clemens, hi Makarius, let me continue concerning syntax:
The current syntax in Tools/interpretation_with_defs.ML is just a proof
of concept:
interpretation L inst
where
"bar = t"
defines f is foo
A much better idea could be to give the new defs in a for-clause:
interpretation L inst
for f :: T
where
"foo = f"
"bar = t"
where the implicit definitions (f) are mentioned in the for-clause.
One could also think about hiding away the full generality of a) from
the user (for which there might be good reasons) and have something like
interpretation L inst
for f :: T
where
f is foo
t is bar
Or the where clause could be integrated completely into the locale
expression using named syntax:
interpretation L (| f := foo, t := bar |)
for f :: T
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
