equal
deleted
inserted
replaced
1546 |
1546 |
1547 If we print out the value of @{ML my_thm} then we see only the |
1547 If we print out the value of @{ML my_thm} then we see only the |
1548 final statement of the theorem. |
1548 final statement of the theorem. |
1549 |
1549 |
1550 @{ML_response_fake [display, gray] |
1550 @{ML_response_fake [display, gray] |
1551 "tracing (string_of_thm @{context} my_thm)" |
1551 "pwriteln (pretty_thm @{context} my_thm)" |
1552 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
1552 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
1553 |
1553 |
1554 However, internally the code-snippet constructs the following |
1554 However, internally the code-snippet constructs the following |
1555 proof. |
1555 proof. |
1556 |
1556 |
1767 unfold the constant @{term "True"} according to its definition (Line 2). |
1767 unfold the constant @{term "True"} according to its definition (Line 2). |
1768 |
1768 |
1769 @{ML_response_fake [display,gray,linenos] |
1769 @{ML_response_fake [display,gray,linenos] |
1770 "Thm.reflexive @{cterm \"True\"} |
1770 "Thm.reflexive @{cterm \"True\"} |
1771 |> Simplifier.rewrite_rule [@{thm True_def}] |
1771 |> Simplifier.rewrite_rule [@{thm True_def}] |
1772 |> string_of_thm @{context} |
1772 |> pretty_thm @{context} |
1773 |> tracing" |
1773 |> pwriteln" |
1774 "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"} |
1774 "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"} |
1775 |
1775 |
1776 Often it is necessary to transform theorems to and from the object |
1776 Often it is necessary to transform theorems to and from the object |
1777 logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} |
1777 logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} |
1778 and @{text "\<And>"}, or the other way around. A reason for such a transformation |
1778 and @{text "\<And>"}, or the other way around. A reason for such a transformation |