equal
deleted
inserted
replaced
3 uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML" |
3 uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML" |
4 begin |
4 begin |
5 |
5 |
6 ML {* no_document use_thys |
6 ML {* no_document use_thys |
7 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
7 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
8 "~~/src/HOL/Reflection/Ferrack"] *} |
8 "~~/src/HOL/Decision_Procs/Ferrack"] *} |
9 |
9 |
10 ML_val {* Code_Target.code_width := 74 *} |
10 ML_val {* Code_Target.code_width := 74 *} |
11 |
11 |
12 end |
12 end |