equal
deleted
inserted
replaced
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* A huge collection of equations to generate code from *} |
|
5 |
|
6 theory Codegenerator_Candidates |
|
7 imports |
|
8 Complex_Main |
|
9 AssocList |
|
10 Binomial |
|
11 "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" |
|
12 Dlist |
|
13 Fset |
|
14 Enum |
|
15 List_Prefix |
|
16 More_List |
|
17 Nat_Infinity |
|
18 Nested_Environment |
|
19 Option_ord |
|
20 Permutation |
|
21 "~~/src/HOL/Number_Theory/Primes" |
|
22 Product_ord |
|
23 "~~/src/HOL/ex/Records" |
|
24 RBT |
|
25 SetsAndFunctions |
|
26 While_Combinator |
|
27 begin |
|
28 |
|
29 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
30 empty: "sublist [] xs" |
|
31 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |
|
32 | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
|
33 |
|
34 code_pred sublist . |
|
35 |
|
36 (*avoid popular infix*) |
|
37 code_reserved SML upto |
|
38 |
|
39 end |
|