44 of rules declared for simplifications. |
44 of rules declared for simplifications. |
45 |
45 |
46 \begin{description} |
46 \begin{description} |
47 |
47 |
48 \item @{command "print_theory"} prints the main logical content of |
48 \item @{command "print_theory"} prints the main logical content of |
49 the theory context; the ``@{text "!"}'' option indicates extra |
49 the background theory; the ``@{text "!"}'' option indicates extra |
50 verbosity. |
50 verbosity. |
51 |
51 |
52 \item @{command "print_methods"} prints all proof methods |
52 \item @{command "print_methods"} prints all proof methods |
53 available in the current theory context. |
53 available in the current theory context. |
54 |
54 |
55 \item @{command "print_attributes"} prints all attributes |
55 \item @{command "print_attributes"} prints all attributes |
56 available in the current theory context. |
56 available in the current theory context. |
57 |
57 |
58 \item @{command "print_theorems"} prints theorems resulting from the |
58 \item @{command "print_theorems"} prints theorems of the background |
59 last command; the ``@{text "!"}'' option indicates extra verbosity. |
59 theory resulting from the last command; the ``@{text "!"}'' option |
|
60 indicates extra verbosity. |
60 |
61 |
61 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
62 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
62 from the theory or proof context matching all of given search |
63 from the theory or proof context matching all of given search |
63 criteria. The criterion @{text "name: p"} selects all theorems |
64 criteria. The criterion @{text "name: p"} selects all theorems |
64 whose fully qualified name matches pattern @{text p}, which may |
65 whose fully qualified name matches pattern @{text p}, which may |