| changeset 7142 | 89e0ff71d113 |
| parent 7072 | c3f3fd86e11c |
| child 7237 | 2919daadba91 |
| 7141:a67dde8820c0 | 7142:89e0ff71d113 |
|---|---|
73 use "simproc.ML"; |
73 use "simproc.ML"; |
74 use_thy "NatBin"; |
74 use_thy "NatBin"; |
75 use "bin_simprocs.ML"; |
75 use "bin_simprocs.ML"; |
76 cd ".."; |
76 cd ".."; |
77 |
77 |
78 use "Tools/svc_funcs.ML"; |
|
79 use_thy "SVC_Oracle"; |
|
80 |
|
78 (*the all-in-one theory*) |
81 (*the all-in-one theory*) |
79 use_thy "Main"; |
82 use_thy "Main"; |
80 |
83 |
81 print_depth 8; |
84 print_depth 8; |
82 |
85 |