equal
deleted
inserted
replaced
1091 Goal.prove @{context} [\"P\"] [] trm tac |
1091 Goal.prove @{context} [\"P\"] [] trm tac |
1092 end" |
1092 end" |
1093 "?P \<Longrightarrow> ?P"} |
1093 "?P \<Longrightarrow> ?P"} |
1094 |
1094 |
1095 This function takes first a context and second a list of strings. This list |
1095 This function takes first a context and second a list of strings. This list |
1096 specifies which variables should be turned into meta-variables once the term |
1096 specifies which variables should be turned into schematic variables once the term |
1097 is proved. The fourth argument is the term to be proved. The fifth is a |
1097 is proved. The fourth argument is the term to be proved. The fifth is a |
1098 corresponding proof given in form of a tactic (we explain tactics in |
1098 corresponding proof given in form of a tactic (we explain tactics in |
1099 Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem |
1099 Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem |
1100 by assumption. As before this code will produce a theorem, but the theorem |
1100 by assumption. As before this code will produce a theorem, but the theorem |
1101 is not yet stored in the theorem database. |
1101 is not yet stored in the theorem database. |