equal
deleted
inserted
replaced
1 theory Setup |
1 theory Setup |
2 imports Complex_Main More_List RBT Dlist Mapping |
2 imports |
|
3 Complex_Main |
|
4 More_List RBT Dlist Mapping |
3 uses |
5 uses |
4 "../../antiquote_setup.ML" |
6 "../../antiquote_setup.ML" |
5 "../../more_antiquote.ML" |
7 "../../more_antiquote.ML" |
6 begin |
8 begin |
7 |
|
8 ML {* no_document use_thys |
|
9 ["Efficient_Nat", "Code_Char_chr", "Product_ord", |
|
10 "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
|
11 "~~/src/HOL/Decision_Procs/Ferrack"] *} |
|
12 |
9 |
13 setup {* |
10 setup {* |
14 let |
11 let |
15 val typ = Simple_Syntax.read_typ; |
12 val typ = Simple_Syntax.read_typ; |
16 val typeT = Syntax.typeT; |
13 val typeT = Syntax.typeT; |