equal
deleted
inserted
replaced
396 If a locale has neither assumptions nor import, no predicate is |
396 If a locale has neither assumptions nor import, no predicate is |
397 defined. If a locale has import but no assumptions, only the locale |
397 defined. If a locale has import but no assumptions, only the locale |
398 predicate is defined. |
398 predicate is defined. |
399 *} |
399 *} |
400 (*<*) |
400 (*<*) |
401 ML_setup {* |
401 ML {* |
402 val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms"; |
402 val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms"; |
403 bind_thm ("comm_semi_ax1", comm_semi_ax1); |
403 bind_thm ("comm_semi_ax1", comm_semi_ax1); |
404 bind_thm ("comm_semi_ax2", comm_semi_ax2); |
404 bind_thm ("comm_semi_ax2", comm_semi_ax2); |
405 *} |
405 *} |
406 (*>*) |
406 (*>*) |