equal
deleted
inserted
replaced
2 imports Complex_Main |
2 imports Complex_Main |
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", "Imperative_HOL", |
7 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
8 "~~/src/HOL/ex/ReflectedFerrack"] *} |
8 "~~/src/HOL/ex/ReflectedFerrack"] *} |
9 |
9 |
10 ML_val {* Code_Target.code_width := 74 *} |
10 ML_val {* Code_Target.code_width := 74 *} |
11 |
11 |
12 end |
12 end |