equal
deleted
inserted
replaced
1553 the following transfer domain rule: \<open>Domainp ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules |
1553 the following transfer domain rule: \<open>Domainp ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules |
1554 allow the package to produce more readable transferred goals, e.g.\ when |
1554 allow the package to produce more readable transferred goals, e.g.\ when |
1555 quantifiers are transferred. |
1555 quantifiers are transferred. |
1556 |
1556 |
1557 \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for |
1557 \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for |
1558 relators of various type constructors, e.g. @{term "rel_set (op =) = (op |
1558 relators of various type constructors, e.g. @{term "rel_set (op =) = (op =)"}. |
1559 =)"}. The @{method (HOL) transfer} method uses these lemmas to infer |
1559 The @{method (HOL) transfer} method uses these lemmas to infer |
1560 transfer rules for non-polymorphic constants on the fly. For examples see |
1560 transfer rules for non-polymorphic constants on the fly. For examples see |
1561 \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property |
1561 \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property |
1562 is proved automatically if the involved type is BNF without dead variables. |
1562 is proved automatically if the involved type is BNF without dead variables. |
1563 |
1563 |
1564 \<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules |
1564 \<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules |