diff --git a/README.md b/README.md index 3af464c..1463b7d 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,14 @@ older versions might be available on a dedicated branch. that provides a simple way for specifying assertions that Isabelle checks while processing a theory. +* [hiding_type_variables.thy](hiding_type_variables.thy) provides + print a setup for defining default type variables of type + constructors. The default type variables can be hidden in output, + e.g., `('a, 'b, 'c) foo` is shown as `_ foo`. This shorthand + notation can also be used in input (using a parse translation), + which (sometimes) helps to focus on the important parts of complex + type declarations. + ## Authors Main author: [Achim D. Brucker](http://www.brucker.ch/) diff --git a/ROOT b/ROOT index 1e88a36..739a13c 100644 --- a/ROOT +++ b/ROOT @@ -1,4 +1,5 @@ session "isabelle-hacks" = "HOL" + options [document = false] theories - assert \ No newline at end of file + assert + hiding_type_variables