From [*The Isabelle Cookbook*](http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/), pages 11 and 12, I found some beginning information related to what I'm trying to do.

Representative of what I'm trying to do is this ML statement:

```
val syntax_str = Syntax.string_of_term @{context} (prop_of @{thm conjI});

```

I want to save the theorem `conjI` to a file as an ASCII string, and have it look like this:

```
P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q

```

Below, I show some of the ML commands I experimented with from [src/Pure/General/pretty.ML](http://isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/Pure/General/pretty.ML) and [src/Pure/Syntax/syntax.ML](http://isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/Pure/Syntax/syntax.ML).

I can get a string, but it's not good for saving to a file. I don't know how to get the string as what's saved to a THY file.

```
ML‹Syntax.pretty_term›
ML‹Syntax.pretty_term @{context} (prop_of @{thm conjI})›
ML‹Pretty.writeln (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.string_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.symbolic_output (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.symbolic_string_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.str_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›

ML‹
  val syntax_str = Syntax.string_of_term @{context} (prop_of @{thm conjI});
  writeln syntax_str;
  File.write (Path.explode (
    File.platform_path(Resources.master_directory @{theory}) ^ 
    "/syntax_str.txt")) syntax_str;
› 
ML‹
  val pretty_str = Pretty.str_of (
    Syntax.pretty_term @{context} (prop_of @{thm conjI}));
  writeln pretty_str;
  File.write (Path.explode (
    File.platform_path(Resources.master_directory @{theory}) ^ 
    "/pretty_str.txt")) pretty_str;
›

```

Thanks.