diff --git a/assert.thy b/Assert.thy similarity index 99% rename from assert.thy rename to Assert.thy index 4cbca12..ab080b0 100644 --- a/assert.thy +++ b/Assert.thy @@ -29,7 +29,7 @@ chapter\An Assertion Framework for Isabelle\ theory - "assert" + "Assert" imports Main keywords diff --git a/hiding_type_variables.thy b/Hiding_Type_Variables.thy similarity index 99% rename from hiding_type_variables.thy rename to Hiding_Type_Variables.thy index 7e498dd..51a271c 100644 --- a/hiding_type_variables.thy +++ b/Hiding_Type_Variables.thy @@ -30,9 +30,9 @@ chapter\Using Print and Parse Translations for Hiding Type Variables\ theory - "hiding_type_variables" + "Hiding_Type_Variables" imports - "assert" (* Can be replaced by Main, after removing all assertions. *) + "Assert" (* Can be replaced by Main, after removing all assertions. *) keywords "register_default_tvars" "update_default_tvars_mode"::thy_decl diff --git a/README.md b/README.md index 13033d4..6e70df2 100644 --- a/README.md +++ b/README.md @@ -10,11 +10,11 @@ older versions might be available on a dedicated branch. ## List of Isabelle Hacks -* [assert.thy](assert.thy) provides a new top level command **assert** +* [Assert.thy](Assert.thy) provides a new top level command **assert** that provides a simple way for specifying assertions that Isabelle checks while processing a theory. -* [hiding_type_variables.thy](hiding_type_variables.thy) provides +* [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 diff --git a/ROOT b/ROOT index 739a13c..2aee2ca 100644 --- a/ROOT +++ b/ROOT @@ -1,5 +1,5 @@ session "isabelle-hacks" = "HOL" + options [document = false] theories - assert - hiding_type_variables + Assert + Hiding_Type_Variables