equal
deleted
inserted
replaced
70 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ); |
70 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ); |
71 |
71 |
72 pretty types: |
72 pretty types: |
73 PolyML.addPrettyPrinter |
73 PolyML.addPrettyPrinter |
74 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
74 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
75 print_depth 99; |
75 print_depth 3; |
76 *) |
76 *) |
77 "===== extend parse to string with markup==="; |
77 "===== extend parse to string with markup==="; |
78 (* |
78 (* |
79 fun parse thy str = |
79 fun parse thy str = |
80 (let val t = (typ_a2real o numbers_to_string) |
80 (let val t = (typ_a2real o numbers_to_string) |