equal
deleted
inserted
replaced
2 imports |
2 imports |
3 Complex_Main |
3 Complex_Main |
4 "~~/src/HOL/Library/Dlist" |
4 "~~/src/HOL/Library/Dlist" |
5 "~~/src/HOL/Library/RBT" |
5 "~~/src/HOL/Library/RBT" |
6 "~~/src/HOL/Library/Mapping" |
6 "~~/src/HOL/Library/Mapping" |
|
7 "~~/src/HOL/Library/IArray" |
7 begin |
8 begin |
8 |
9 |
9 (* FIXME avoid writing into source directory *) |
10 (* FIXME avoid writing into source directory *) |
10 ML {* |
11 ML {* |
11 Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples")) |
12 Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples")) |