| author | huffman | 
| Mon, 07 Mar 2005 23:54:01 +0100 | |
| changeset 15587 | f363e6e080e7 | 
| parent 14981 | e73f8140af78 | 
| permissions | -rw-r--r-- | 
| 5950 | 1 | (* Title: Pure/Isar/isar.ML | 
| 2 | ID: $Id$ | |
| 3 | Author: Markus Wenzel, TU Muenchen | |
| 4 | ||
| 5 | Isabelle/Isar main interface. | |
| 6 | *) | |
| 7 | ||
| 8 | signature ISAR = | |
| 9 | sig | |
| 10 | val main: unit -> unit | |
| 11 | val loop: unit -> unit | |
| 6858 | 12 | val sync_main: unit -> unit | 
| 13 | val sync_loop: unit -> unit | |
| 5950 | 14 | end; | 
| 15 | ||
| 16 | structure Isar: ISAR = | |
| 17 | struct | |
| 18 | ||
| 19 | val main = OuterSyntax.main; | |
| 20 | val loop = OuterSyntax.loop; | |
| 6858 | 21 | val sync_main = OuterSyntax.sync_main; | 
| 22 | val sync_loop = OuterSyntax.sync_loop; | |
| 5950 | 23 | |
| 24 | end; |