equal
deleted
inserted
replaced
1964 @{text "> let \"?case\" = \"?P\""} |
1964 @{text "> let \"?case\" = \"?P\""} |
1965 \end{tabular}*} |
1965 \end{tabular}*} |
1966 |
1966 |
1967 |
1967 |
1968 text {* |
1968 text {* |
1969 One often wants to know the theorems that are used in the proof |
1969 One often wants to know the theorems that are involved in proving |
1970 of a theorem. They can be obtained by introspecting the theorem. |
1970 a theorem. They can be obtained by introspecting the theorem. |
1971 To introspect a theorem, let us define the following three functions that |
1971 To introspect a theorem, let us define the following three functions that |
1972 analyse the @{ML_type_ind proof_body} data-structure from the structure |
1972 analyse the @{ML_type_ind proof_body} data-structure from the structure |
1973 @{ML_struct Proofterm}. |
1973 @{ML_struct Proofterm}. |
1974 *} |
1974 *} |
1975 |
1975 |