ProgTutorial/General.thy
changeset 359 be6538c7b41d
parent 358 9cf3bc448210
child 360 bdd411caf5eb
equal deleted inserted replaced
358:9cf3bc448210 359:be6538c7b41d
  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.