equal
deleted
inserted
replaced
8 ML {* no_document use_thys |
8 ML {* no_document use_thys |
9 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
9 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
10 "~~/src/HOL/Decision_Procs/Ferrack"] *} |
10 "~~/src/HOL/Decision_Procs/Ferrack"] *} |
11 |
11 |
12 ML_command {* Code_Target.code_width := 74 *} |
12 ML_command {* Code_Target.code_width := 74 *} |
13 ML_command {* reset unique_names *} |
13 ML_command {* Unsynchronized.reset unique_names *} |
14 |
14 |
15 end |
15 end |