equal
deleted
inserted
replaced
886 @{ML_response [display,gray] |
886 @{ML_response [display,gray] |
887 "@{binding \"name\"}" |
887 "@{binding \"name\"}" |
888 "name"} |
888 "name"} |
889 |
889 |
890 An example where a qualified name is needed is the function |
890 An example where a qualified name is needed is the function |
891 @{ML_ind define in LocalTheory}. This function is used below to define |
891 @{ML_ind define in Local_Theory}. This function is used below to define |
892 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}. |
892 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}. |
893 *} |
893 *} |
894 |
894 |
895 local_setup %gray {* |
895 local_setup %gray {* |
896 LocalTheory.define Thm.internalK |
896 Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn), |
897 ((@{binding "TrueConj"}, NoSyn), |
|
898 (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *} |
897 (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *} |
899 |
898 |
900 text {* |
899 text {* |
901 Now querying the definition you obtain: |
900 Now querying the definition you obtain: |
902 |
901 |