equal
deleted
inserted
replaced
1603 |
1603 |
1604 @{ML_response [display,gray] |
1604 @{ML_response [display,gray] |
1605 "let |
1605 "let |
1606 fun pred s = match_string \"my_thm_simp\" s |
1606 fun pred s = match_string \"my_thm_simp\" s |
1607 in |
1607 in |
1608 exists pred (get_thm_names_from_ss @{simpset}) |
1608 exists pred (get_thm_names_from_ss @{context}) |
1609 end" |
1609 end" |
1610 "true"} |
1610 "true"} |
1611 |
1611 |
1612 The main point of storing the theorems @{thm [source] my_thm} and @{thm |
1612 The main point of storing the theorems @{thm [source] my_thm} and @{thm |
1613 [source] my_thm_simp} is that they can now also be referenced with the |
1613 [source] my_thm_simp} is that they can now also be referenced with the |
1897 "True = False"} |
1897 "True = False"} |
1898 |
1898 |
1899 \begin{readmore} |
1899 \begin{readmore} |
1900 Functions that setup goal states and prove theorems are implemented in |
1900 Functions that setup goal states and prove theorems are implemented in |
1901 @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to |
1901 @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to |
1902 skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}. |
1902 skip proofs of theorems are implemented in @{ML_file "Pure/skip_proof.ML"}. |
1903 \end{readmore} |
1903 \end{readmore} |
1904 |
1904 |
1905 Theorems also contain auxiliary data, such as the name of the theorem, its |
1905 Theorems also contain auxiliary data, such as the name of the theorem, its |
1906 kind, the names for cases and so on. This data is stored in a string-string |
1906 kind, the names for cases and so on. This data is stored in a string-string |
1907 list and can be retrieved with the function @{ML_ind get_tags in |
1907 list and can be retrieved with the function @{ML_ind get_tags in |