| author | kuncar | 
| Tue, 25 Feb 2014 19:07:14 +0100 | |
| changeset 55736 | f1ed1e9cd080 | 
| parent 30834 | 1640e0625301 | 
| child 57440 | 802d33c46459 | 
| permissions | -rw-r--r-- | 
| 4689 | 1 | |
| 19 | 2 | Pure: The Pure Isabelle System | 
| 0 | 3 | |
| 4689 | 4 | |
| 4620 | 5 | This directory contains the ML source files for Pure Isabelle, which | 
| 16115 | 6 | is the basis for all object-logics. The Isabelle/Pure image may be | 
| 7 | compiled in batch mode like this: | |
| 8 | ||
| 28504 
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
 wenzelm parents: 
16117diff
changeset | 9 | isabelle make Pure | 
| 16115 | 10 | |
| 11 | Developers may want to produce a RAW image that merely consists of the | |
| 12 | ML compiler with the compatibility setup of ML-Systems/ preloaded: | |
| 0 | 13 | |
| 28504 
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
 wenzelm parents: 
16117diff
changeset | 14 | isabelle make RAW | 
| 16115 | 15 | |
| 16 | Now the Pure session may be compiled interactively as follows: | |
| 0 | 17 | |
| 30834 | 18 | isabelle tty -l RAW | 
| 19 | use "ROOT.ML"; | |
| 16115 | 20 |