785 } |
785 } |
786 } |
786 } |
787 } |
787 } |
788 \] |
788 \] |
789 |
789 |
790 While we obtained a theorem as the result, this theorem is not |
790 While we obtained a theorem as result, this theorem is not |
791 yet stored in Isabelle's theorem database. Consequently, it cannot be |
791 yet stored in Isabelle's theorem database. Consequently, it cannot be |
792 referenced later on. One way to store it in the theorem database is |
792 referenced later on. One way to store it in the theorem database is |
793 by using the function @{ML_ind note in LocalTheory}. |
793 by using the function @{ML_ind note in LocalTheory}. |
794 *} |
794 *} |
795 |
795 |
796 local_setup %gray {* |
796 local_setup %gray {* |
797 LocalTheory.note Thm.theoremK |
797 LocalTheory.note Thm.theoremK |
798 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
798 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
799 |
799 |
800 text {* |
800 text {* |
801 Now it can be referenced with the \isacommand{thm}-command on the user-level |
801 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which |
802 of Isabelle |
802 classifies the theorem. For a theorem arising from a definition we should |
|
803 state @{ML_ind definitionK in Thm}, instead. The second argument is the |
|
804 name under which we stroe the theorem or theorems. The third contains is |
|
805 a list of (theorem) attributes. Above it is empty, but if we want to store |
|
806 the therem and at the same time add it to the simpset we have to declare. |
|
807 *} |
|
808 |
|
809 local_setup %gray {* |
|
810 LocalTheory.note Thm.theoremK |
|
811 ((@{binding "my_thm_simp"}, [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
|
812 |
|
813 |
|
814 |
|
815 text {* |
|
816 Now @{thm [source] my_thm} can be referenced with the \isacommand{thm}-command |
|
817 on the user-level of Isabelle |
803 |
818 |
804 \begin{isabelle} |
819 \begin{isabelle} |
805 \isacommand{thm}~@{text "my_thm"}\isanewline |
820 \isacommand{thm}~@{text "my_thm"}\isanewline |
806 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
821 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
807 \end{isabelle} |
822 \end{isabelle} |