equal
deleted
inserted
replaced
2066 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. |
2066 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. |
2067 \end{readmore} |
2067 \end{readmore} |
2068 |
2068 |
2069 *} |
2069 *} |
2070 |
2070 |
2071 |
2071 text {* |
|
2072 (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term} |
|
2073 are of any use/efficient) |
|
2074 *} |
2072 |
2075 |
2073 |
2076 |
2074 section {* Structured Proofs (TBD) *} |
2077 section {* Structured Proofs (TBD) *} |
2075 |
2078 |
2076 text {* TBD *} |
2079 text {* TBD *} |