equal
deleted
inserted
replaced
375 in Pretty.writeln p end; |
375 in Pretty.writeln p end; |
376 |
376 |
377 |
377 |
378 (** Isar setup **) |
378 (** Isar setup **) |
379 |
379 |
380 fun norm_print_term_cmd (modes, raw_t) state = |
380 fun norm_print_term_cmd (modes, s) state = |
381 let val ctxt = Toplevel.context_of state |
381 let val ctxt = Toplevel.context_of state |
382 in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end; |
382 in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; |
383 |
383 |
384 val setup = Theory.add_oracle ("normalization", normalization_oracle) |
384 val setup = Theory.add_oracle ("normalization", normalization_oracle) |
385 |
385 |
386 local structure P = OuterParse and K = OuterKeyword in |
386 local structure P = OuterParse and K = OuterKeyword in |
387 |
387 |