equal
deleted
inserted
replaced
56 val add_trfuns: |
56 val add_trfuns: |
57 (string * (ast list -> ast)) list * |
57 (string * (ast list -> ast)) list * |
58 (string * (term list -> term)) list * |
58 (string * (term list -> term)) list * |
59 (string * (term list -> term)) list * |
59 (string * (term list -> term)) list * |
60 (string * (ast list -> ast)) list -> sg -> sg |
60 (string * (ast list -> ast)) list -> sg -> sg |
|
61 val add_trfunsT: |
|
62 (string * (typ -> term list -> term)) list -> sg -> sg |
61 val add_trrules: (string * string) Syntax.trrule list -> sg -> sg |
63 val add_trrules: (string * string) Syntax.trrule list -> sg -> sg |
62 val add_trrules_i: ast Syntax.trrule list -> sg -> sg |
64 val add_trrules_i: ast Syntax.trrule list -> sg -> sg |
63 val add_name: string -> sg -> sg |
65 val add_name: string -> sg -> sg |
64 val make_draft: sg -> sg |
66 val make_draft: sg -> sg |
65 val merge: sg * sg -> sg |
67 val merge: sg * sg -> sg |
547 val add_syntax = extend_sign ext_syntax "#"; |
549 val add_syntax = extend_sign ext_syntax "#"; |
548 val add_syntax_i = extend_sign ext_syntax_i "#"; |
550 val add_syntax_i = extend_sign ext_syntax_i "#"; |
549 val add_modesyntax = extend_sign ext_modesyntax "#"; |
551 val add_modesyntax = extend_sign ext_modesyntax "#"; |
550 val add_modesyntax_i = extend_sign ext_modesyntax_i "#"; |
552 val add_modesyntax_i = extend_sign ext_modesyntax_i "#"; |
551 val add_trfuns = extend_sign (ext_syn Syntax.extend_trfuns) "#"; |
553 val add_trfuns = extend_sign (ext_syn Syntax.extend_trfuns) "#"; |
|
554 val add_trfunsT = extend_sign (ext_syn Syntax.extend_trfunsT) "#"; |
552 val add_trrules = extend_sign (ext_syn Syntax.extend_trrules) "#"; |
555 val add_trrules = extend_sign (ext_syn Syntax.extend_trrules) "#"; |
553 val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#"; |
556 val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#"; |
554 |
557 |
555 fun add_name name sg = extend_sign K name () sg; |
558 fun add_name name sg = extend_sign K name () sg; |
556 val make_draft = add_name "#"; |
559 val make_draft = add_name "#"; |