equal
deleted
inserted
replaced
1957 |
1957 |
1958 \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem |
1958 \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem |
1959 is a quotient extension theorem. Quotient extension theorems |
1959 is a quotient extension theorem. Quotient extension theorems |
1960 allow for quotienting inside container types. Given a polymorphic |
1960 allow for quotienting inside container types. Given a polymorphic |
1961 type that serves as a container, a map function defined for this |
1961 type that serves as a container, a map function defined for this |
1962 container using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation |
1962 container using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation |
1963 map defined for for the container type, the quotient extension |
1963 map defined for for the container type, the quotient extension |
1964 theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems |
1964 theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient{\isadigit{3}}\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient{\isadigit{3}}\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems |
1965 are stored in a database and are used all the steps of lifting |
1965 are stored in a database and are used all the steps of lifting |
1966 theorems. |
1966 theorems. |
1967 |
1967 |
1968 \end{description}% |
1968 \end{description}% |
1969 \end{isamarkuptext}% |
1969 \end{isamarkuptext}% |
2501 \item[\isa{iterations}] sets how many sets of assignments are |
2501 \item[\isa{iterations}] sets how many sets of assignments are |
2502 generated for each particular size. |
2502 generated for each particular size. |
2503 |
2503 |
2504 \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in |
2504 \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in |
2505 structured proofs should be ignored. |
2505 structured proofs should be ignored. |
|
2506 |
|
2507 \item[\isa{locale}] specifies how to process conjectures in |
|
2508 a locale context, i.e., they can be interpreted or expanded. |
|
2509 The option is a whitespace-separated list of the two words |
|
2510 \isa{interpret} and \isa{expand}. The list determines the |
|
2511 order they are employed. The default setting is to first use |
|
2512 interpretations and then test the expanded conjecture. |
|
2513 The option is only provided as attribute declaration, but not |
|
2514 as parameter to the command. |
2506 |
2515 |
2507 \item[\isa{timeout}] sets the time limit in seconds. |
2516 \item[\isa{timeout}] sets the time limit in seconds. |
2508 |
2517 |
2509 \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to |
2518 \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to |
2510 instantiate type variables. |
2519 instantiate type variables. |