equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Linked Lists by ML references *} |
5 header {* Linked Lists by ML references *} |
6 |
6 |
7 theory Linked_Lists |
7 theory Linked_Lists |
8 imports "../Imperative_HOL" Code_Integer |
8 imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Integer" |
9 begin |
9 begin |
10 |
10 |
11 section {* Definition of Linked Lists *} |
11 section {* Definition of Linked Lists *} |
12 |
12 |
13 setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *} |
13 setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *} |
1001 ML {* @{code test_3} () *} |
1001 ML {* @{code test_3} () *} |
1002 |
1002 |
1003 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? |
1003 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? |
1004 |
1004 |
1005 end |
1005 end |
|
1006 |