equal
deleted
inserted
replaced
92 theory -> thm list * theory |
92 theory -> thm list * theory |
93 val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list -> |
93 val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list -> |
94 theory -> thm list * theory |
94 theory -> thm list * theory |
95 val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list -> |
95 val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list -> |
96 theory -> thm list * theory |
96 theory -> thm list * theory |
97 val add_defss: bool -> ((bstring * string list) * attribute list) list -> |
|
98 theory -> thm list list * theory |
|
99 val add_defss_i: bool -> ((bstring * term list) * attribute list) list -> |
|
100 theory -> thm list list * theory |
|
101 val appl_syntax: (string * typ * mixfix) list |
97 val appl_syntax: (string * typ * mixfix) list |
102 val applC_syntax: (string * typ * mixfix) list |
98 val applC_syntax: (string * typ * mixfix) list |
103 end; |
99 end; |
104 |
100 |
105 structure PureThy: PURE_THY = |
101 structure PureThy: PURE_THY = |
487 val add_axiomss_i = add_multis Theory.add_axioms_i; |
483 val add_axiomss_i = add_multis Theory.add_axioms_i; |
488 val add_defs = add_singles o Theory.add_defs false; |
484 val add_defs = add_singles o Theory.add_defs false; |
489 val add_defs_i = add_singles o Theory.add_defs_i false; |
485 val add_defs_i = add_singles o Theory.add_defs_i false; |
490 val add_defs_unchecked = add_singles o Theory.add_defs true; |
486 val add_defs_unchecked = add_singles o Theory.add_defs true; |
491 val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; |
487 val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; |
492 val add_defss = add_multis o Theory.add_defs false; |
|
493 val add_defss_i = add_multis o Theory.add_defs_i false; |
|
494 end; |
488 end; |
495 |
489 |
496 |
490 |
497 (* simple interface for simple definitions *) |
491 (* simple interface for simple definitions *) |
498 |
492 |