On 16/09/18 15:24, Florian Haftmann wrote: > > I guess this had something to do with Haskabelle, taking into account > its fundamental design flaw to write terms on its own rather than having > Isabelle's existing printing doing the job. > > Since there is no reference left, it can be safely discarded. >> >> The motivation behind the question: slightly more high-level access to >> notation, e.g. for export to other languages; possibly without "fishing" >> in the generated grammar.
OK, I will replace it by something that I can use for the purpose of exporting theory content. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev