adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Updated various legacy notations.

This commit is contained in:
Achim D. Brucker 2018-12-24 09:00:31 +00:00
parent 818438f2cf
commit f8f04dd867
2 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Assert.thy
View File

@ -223,14 +223,14 @@ structure String_of_thm_cmp_assert : STRING_OF_THM_CMP_ASSERT = struct
name = "string_of_thm_equal", name = "string_of_thm_equal",
description = "Check that string representation (including types) " description = "Check that string representation (including types) "
^"matches given string.", ^"matches given string.",
assertion = (assert_string_of_thm_cmp_args (op =)) assertion = (assert_string_of_thm_cmp_args (=))
} }
val string_of_thm_notequal = { val string_of_thm_notequal = {
name = "string_of_thm_notequal", name = "string_of_thm_notequal",
description = "Check that string representation (including types) " description = "Check that string representation (including types) "
^"does not match given string.", ^"does not match given string.",
assertion = (assert_string_of_thm_cmp_args (op <>)) assertion = (assert_string_of_thm_cmp_args (<>))
} }
end end
\<close> \<close>

16
Hiding_Type_Variables.thy
View File

@ -42,21 +42,21 @@ text\<open>
This theory implements a mechanism for declaring default type variables for This theory implements a mechanism for declaring default type variables for
data types. This comes handy for complex data types with many type variables. data types. This comes handy for complex data types with many type variables.
The theory sets up both configurable print and parse translations that allows The theory sets up both configurable print and parse translations that allows
for replacing @{emph \<open>all\<close>} type variables by @{text \<open>(_)\<close>}, e.g., a five-ary for replacing @{emph \<open>all\<close>} type variables by \<open>(_)\<close>, e.g., a five-ary
constructor @{text \<open>('a, 'b, 'c, 'd, 'e) hide_tvar_foo\<close>} can be shorted to constructor \<open>('a, 'b, 'c, 'd, 'e) hide_tvar_foo\<close> can be shorted to
@{text \<open>(_) hide_tvar_foo\<close>}. The use of this shorthand in output (printing) and input \<open>(_) hide_tvar_foo\<close>. The use of this shorthand in output (printing) and input
(parsing) is, on a per-type basis, user-configurable using the top-level (parsing) is, on a per-type basis, user-configurable using the top-level
commands @{text \<open>register_default_tvars\<close>} (for registering the names of the commands \<open>register_default_tvars\<close> (for registering the names of the
default type variables and the print/parse mode) and default type variables and the print/parse mode) and
@{text \<open>update_default_tvars_mode\<close>} (for changing the print/parse mode \<open>update_default_tvars_mode\<close> (for changing the print/parse mode
dynamically). dynamically).
The input also supports short-hands for declaring default sorts (e.g., The input also supports short-hands for declaring default sorts (e.g.,
@{text \<open>(_::linorder)\<close>} specifies that all default variables need to be \<open>(_::linorder)\<close> specifies that all default variables need to be
instances of the sort (type class) @{class \<open>linorder\<close>} and short-hands instances of the sort (type class) @{class \<open>linorder\<close>} and short-hands
of overriding a suffice (or prefix) of the default type variables. For of overriding a suffice (or prefix) of the default type variables. For
example, @{text \<open>('state) hide_tvar_foo _.\<close>} is a short-hand for example, \<open>('state) hide_tvar_foo _.\<close> is a short-hand for
@{text \<open>('a, 'b, 'c, 'd, 'state) hide_tvar_foo\<close>}. \<open>('a, 'b, 'c, 'd, 'state) hide_tvar_foo\<close>.
}\<close> }\<close>
section\<open>Implementation\<close> section\<open>Implementation\<close>