equal
deleted
inserted
replaced
35 |
35 |
36 text {* |
36 text {* |
37 It returns the definition (as a theorem) and the local theory in which the |
37 It returns the definition (as a theorem) and the local theory in which the |
38 definition has been made. In Line 4, @{ML_ind internalK in Thm} is a flag |
38 definition has been made. In Line 4, @{ML_ind internalK in Thm} is a flag |
39 attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} |
39 attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} |
40 and @{ML_ind axiomK in Thm}). These flags just classify theorems and have no |
40 and @{ML_ind axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.} |
|
41 These flags just classify theorems and have no |
41 significant meaning, except for tools that, for example, find theorems in |
42 significant meaning, except for tools that, for example, find theorems in |
42 the theorem database.\footnote{FIXME: put in the section about theorems.} We |
43 the theorem database.\footnote{FIXME: put in the section about theorems.} We |
43 also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for |
44 also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for |
44 our inductive predicates are not meant to be seen by the user and therefore |
45 our inductive predicates are not meant to be seen by the user and therefore |
45 do not need to have any theorem attributes. A testcase for this function is |
46 do not need to have any theorem attributes. A testcase for this function is |