equal
deleted
inserted
replaced
1 theory ToyList |
1 theory ToyList |
2 imports Datatype |
2 imports Datatype |
3 begin |
3 begin |
4 |
4 |
5 (*<*) |
5 (*<*) |
6 ML {* |
6 ML {* (* FIXME somewhat non-standard, fragile *) |
7 let |
7 let |
8 val texts = |
8 val texts = |
9 map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) |
9 map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) |
10 ["ToyList1", "ToyList2"]; |
10 ["ToyList1", "ToyList2"]; |
11 val trs = Outer_Syntax.parse Position.start (implode texts); |
11 val trs = Outer_Syntax.parse Position.start (implode texts); |
12 in @{assert} (Toplevel.is_toplevel (fold Toplevel.command trs Toplevel.toplevel)) end; |
12 val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; |
|
13 in @{assert} (Toplevel.is_toplevel end_state) end; |
13 *} |
14 *} |
14 (*>*) |
15 (*>*) |
15 |
16 |
16 text{*\noindent |
17 text{*\noindent |
17 HOL already has a predefined theory of lists called @{text List} --- |
18 HOL already has a predefined theory of lists called @{text List} --- |