1216 |
1216 |
1217 * ML within Isar: antiquotations allow to embed statically-checked |
1217 * ML within Isar: antiquotations allow to embed statically-checked |
1218 formal entities in the source, referring to the context available at |
1218 formal entities in the source, referring to the context available at |
1219 compile-time. For example: |
1219 compile-time. For example: |
1220 |
1220 |
|
1221 ML {* @{sort "{zero,one}"} *} |
1221 ML {* @{typ "'a => 'b"} *} |
1222 ML {* @{typ "'a => 'b"} *} |
1222 ML {* @{term "%x. x"} *} |
1223 ML {* @{term "%x. x"} *} |
1223 ML {* @{prop "x == y"} *} |
1224 ML {* @{prop "x == y"} *} |
1224 ML {* @{ctyp "'a => 'b"} *} |
1225 ML {* @{ctyp "'a => 'b"} *} |
1225 ML {* @{cterm "%x. x"} *} |
1226 ML {* @{cterm "%x. x"} *} |
1226 ML {* @{cprop "x == y"} *} |
1227 ML {* @{cprop "x == y"} *} |
1227 ML {* @{thm asm_rl} *} |
1228 ML {* @{thm asm_rl} *} |
1228 ML {* @{thms asm_rl} *} |
1229 ML {* @{thms asm_rl} *} |
1229 ML {* @{type_name c} *} |
1230 ML {* @{type_name c} *} |
|
1231 ML {* @{type_syntax c} *} |
1230 ML {* @{const_name c} *} |
1232 ML {* @{const_name c} *} |
1231 ML {* @{const_syntax c} *} |
1233 ML {* @{const_syntax c} *} |
1232 ML {* @{context} *} |
1234 ML {* @{context} *} |
1233 ML {* @{theory} *} |
1235 ML {* @{theory} *} |
1234 ML {* @{theory Pure} *} |
1236 ML {* @{theory Pure} *} |