| 5950 |      1 | (*  Title:      Pure/Isar/isar.ML
 | 
|  |      2 |     ID:         $Id$
 | 
|  |      3 |     Author:     Markus Wenzel, TU Muenchen
 | 
| 8807 |      4 |     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 | 
| 5950 |      5 | 
 | 
|  |      6 | Isabelle/Isar main interface.
 | 
|  |      7 | *)
 | 
|  |      8 | 
 | 
|  |      9 | signature ISAR =
 | 
|  |     10 | sig
 | 
|  |     11 |   val main: unit -> unit
 | 
|  |     12 |   val loop: unit -> unit
 | 
| 6858 |     13 |   val sync_main: unit -> unit
 | 
|  |     14 |   val sync_loop: unit -> unit
 | 
| 5950 |     15 | end;
 | 
|  |     16 | 
 | 
|  |     17 | structure Isar: ISAR =
 | 
|  |     18 | struct
 | 
|  |     19 | 
 | 
|  |     20 | val main = OuterSyntax.main;
 | 
|  |     21 | val loop = OuterSyntax.loop;
 | 
| 6858 |     22 | val sync_main = OuterSyntax.sync_main;
 | 
|  |     23 | val sync_loop = OuterSyntax.sync_loop;
 | 
| 5950 |     24 | 
 | 
|  |     25 | end;
 |