author | hoelzl |
Wed, 10 Oct 2012 12:12:24 +0200 | |
changeset 49785 | 0a8adca22974 |
parent 49077 | 154f25a162e3 |
child 51160 | 599ff65b85e2 |
permissions | -rw-r--r-- |
31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
21917 | 3 |
|
31378 | 4 |
header {* A huge collection of equations to generate code from *} |
21917 | 5 |
|
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37407
diff
changeset
|
6 |
theory Candidates |
21917 | 7 |
imports |
27421 | 8 |
Complex_Main |
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37407
diff
changeset
|
9 |
Library |
49077
154f25a162e3
renamed theory List_Prefix into Sublist (since it is not only about prefixes)
Christian Sternagel
parents:
41884
diff
changeset
|
10 |
"~~/src/HOL/Library/Sublist" |
32479 | 11 |
"~~/src/HOL/Number_Theory/Primes" |
35303 | 12 |
"~~/src/HOL/ex/Records" |
21917 | 13 |
begin |
14 |
||
33500 | 15 |
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
16 |
empty: "sublist [] xs" |
|
17 |
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |
|
18 |
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
|
19 |
||
20 |
code_pred sublist . |
|
21 |
||
33042 | 22 |
(*avoid popular infix*) |
23 |
code_reserved SML upto |
|
31378 | 24 |
|
21917 | 25 |
end |