--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:14 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:15 2014 +0200
@@ -1596,7 +1596,7 @@
@{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
- @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\
@{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
@{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
@{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
@@ -1733,11 +1733,11 @@
"~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
in the same directory.
- \item @{attribute (HOL) invariant_commute} registers a theorem that
+ \item @{attribute (HOL) relator_eq_onp} registers a theorem that
shows a relationship between the constant @{text
- Lifting.invariant} (used for internal encoding of proper subtypes)
+ eq_onp} (used for internal encoding of proper subtypes)
and a relator. Such theorems allows the package to hide @{text
- Lifting.invariant} from a user in a user-readable form of a
+ eq_onp} from a user in a user-readable form of a
respectfulness theorem. For examples see @{file
"~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.