equal
deleted
inserted
replaced
1683 \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.} |
1683 \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.} |
1684 |
1684 |
1685 Theorems can also be produced from terms by giving an explicit proof. |
1685 Theorems can also be produced from terms by giving an explicit proof. |
1686 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1686 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1687 in the structure @{ML_struct Goal}. For example below we use this function |
1687 in the structure @{ML_struct Goal}. For example below we use this function |
1688 to prove the term @{term "P \<Longrightarrow> P"}. |
1688 to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?} |
1689 |
1689 |
1690 @{ML_response_fake [display,gray] |
1690 @{ML_response_fake [display,gray] |
1691 "let |
1691 "let |
1692 val trm = @{term \"P \<Longrightarrow> P::bool\"} |
1692 val trm = @{term \"P \<Longrightarrow> P::bool\"} |
1693 val tac = K (atac 1) |
1693 val tac = K (atac 1) |