equal
deleted
inserted
replaced
19 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
19 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
20 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
20 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
21 \end{matharray} |
21 \end{matharray} |
22 |
22 |
23 \begin{rail} |
23 \begin{rail} |
24 'print\_theory' ( '!'?) |
24 ('print\_theory' | 'print\_theorems') ('!'?) |
25 ; |
25 ; |
26 |
26 |
27 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *) |
27 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *) |
28 ; |
28 ; |
29 thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | |
29 thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | |
54 available in the current theory context. |
54 available in the current theory context. |
55 |
55 |
56 \item @{command "print_attributes"} prints all attributes |
56 \item @{command "print_attributes"} prints all attributes |
57 available in the current theory context. |
57 available in the current theory context. |
58 |
58 |
59 \item @{command "print_theorems"} prints theorems resulting from |
59 \item @{command "print_theorems"} prints theorems resulting from the |
60 the last command. |
60 last command; the ``@{text "!"}'' option indicates extra verbosity. |
61 |
61 |
62 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
62 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
63 from the theory or proof context matching all of given search |
63 from the theory or proof context matching all of given search |
64 criteria. The criterion @{text "name: p"} selects all theorems |
64 criteria. The criterion @{text "name: p"} selects all theorems |
65 whose fully qualified name matches pattern @{text p}, which may |
65 whose fully qualified name matches pattern @{text p}, which may |