equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 HOL_build_completed; (*Make examples fail if HOL did*) |
7 HOL_build_completed; (*Make examples fail if HOL did*) |
8 |
8 |
9 use_thy"AutoChopper"; |
9 use_thy"AutoChopper"; |
|
10 use_thy"AutoChopper1"; |
|
11 use_thy"Regset_of_auto"; |