equal
deleted
inserted
replaced
960 text {* |
960 text {* |
961 A word of warning: such references must not be used in any code that |
961 A word of warning: such references must not be used in any code that |
962 is meant to be more than just for testing purposes! Here it is only used |
962 is meant to be more than just for testing purposes! Here it is only used |
963 to illustrate matters. We will show later how to store data properly without |
963 to illustrate matters. We will show later how to store data properly without |
964 using references. The function @{ML Thm.declaration_attribute} expects us to |
964 using references. The function @{ML Thm.declaration_attribute} expects us to |
965 provide two functions that add and delete theorems from this list. At |
965 provide two functions that add and delete theorems from this list. |
966 the moment we use the two functions: |
966 For this we use the two functions: |
967 *} |
967 *} |
968 |
968 |
969 ML{*fun my_thms_add thm ctxt = |
969 ML{*fun my_thms_add thm ctxt = |
970 (my_thms := Thm.add_thm thm (!my_thms); ctxt) |
970 (my_thms := Thm.add_thm thm (!my_thms); ctxt) |
971 |
971 |
1112 For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also |
1112 For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also |
1113 the recipe in Section~\ref{recipe:storingdata} about storing arbitrary |
1113 the recipe in Section~\ref{recipe:storingdata} about storing arbitrary |
1114 data. |
1114 data. |
1115 \end{readmore} |
1115 \end{readmore} |
1116 |
1116 |
1117 What are: |
1117 (FIXME What are: |
1118 |
1118 |
1119 @{text "theory_attributes"} |
1119 @{text "theory_attributes"} |
1120 @{text "proof_attributes"} |
1120 @{text "proof_attributes"}) |
1121 |
1121 |
1122 |
1122 |
1123 \begin{readmore} |
1123 \begin{readmore} |
1124 FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"} |
1124 FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"} |
1125 \end{readmore} |
1125 \end{readmore} |
1126 *} |
1126 *} |
1127 |
1127 |
1128 |
1128 |
1129 section {* Theories, Contexts and Local Theories *} |
1129 section {* Theories, Contexts and Local Theories (TBD) *} |
1130 |
1130 |
1131 text {* |
1131 text {* |
1132 (FIXME: expand) |
1132 (FIXME: expand) |
1133 |
1133 |
1134 (FIXME: explain \isacommand{setup}) |
1134 (FIXME: explain \isacommand{setup}) |
1146 |
1146 |
1147 *} |
1147 *} |
1148 |
1148 |
1149 |
1149 |
1150 |
1150 |
1151 section {* Storing Theorems\label{sec:storing} *} |
1151 section {* Storing Theorems\label{sec:storing} (TBD) *} |
1152 |
1152 |
1153 text {* @{ML PureThy.add_thms_dynamic} *} |
1153 text {* @{ML PureThy.add_thms_dynamic} *} |
1154 |
1154 |
1155 |
1155 |
1156 |
1156 |
1176 done |
1176 done |
1177 |
1177 |
1178 thm foo_def |
1178 thm foo_def |
1179 (*>*) |
1179 (*>*) |
1180 |
1180 |
1181 section {* Misc *} |
1181 section {* Pretty-Printing (TBD) *} |
|
1182 |
|
1183 text {* |
|
1184 @{ML Pretty.big_list} |
|
1185 *} |
|
1186 |
|
1187 section {* Misc (TBD) *} |
1182 |
1188 |
1183 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |
1189 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |
1184 |
1190 |
1185 end |
1191 end |