Renamed theories to comply to Isabelle's naming convention.
This commit is contained in:
parent
9bfbf12444
commit
3b0a88dfa6
|
@ -29,7 +29,7 @@
|
|||
|
||||
chapter\<open>An Assertion Framework for Isabelle\<close>
|
||||
theory
|
||||
"assert"
|
||||
"Assert"
|
||||
imports
|
||||
Main
|
||||
keywords
|
|
@ -30,9 +30,9 @@
|
|||
|
||||
chapter\<open>Using Print and Parse Translations for Hiding Type Variables\<close>
|
||||
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
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue