1signature GrammarDeltas = 2sig 3 4 val thy_deltas : {thyname : string} -> 5 type_grammar.delta list * term_grammar.user_delta list 6 val record_tmdelta : term_grammar.user_delta -> unit 7 val record_tydelta : type_grammar.delta -> unit 8 9end 10
1signature GrammarDeltas = 2sig 3 4 val thy_deltas : {thyname : string} -> 5 type_grammar.delta list * term_grammar.user_delta list 6 val record_tmdelta : term_grammar.user_delta -> unit 7 val record_tydelta : type_grammar.delta -> unit 8 9end 10