| author | bulwahn |
| Wed, 20 Jan 2010 18:08:08 +0100 | |
| changeset 34953 | a053ad2a7a72 |
| parent 33500 | 22e5725be1f3 |
| child 35303 | 816e48d60b13 |
| 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 |
|
| 31378 | 6 |
theory Codegenerator_Candidates |
| 21917 | 7 |
imports |
| 27421 | 8 |
Complex_Main |
| 21917 | 9 |
AssocList |
10 |
Binomial |
|
| 31849 | 11 |
Fset |
| 27421 | 12 |
Enum |
| 21917 | 13 |
List_Prefix |
14 |
Nat_Infinity |
|
|
24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
24423
diff
changeset
|
15 |
Nested_Environment |
| 26515 | 16 |
Option_ord |
| 21917 | 17 |
Permutation |
| 32479 | 18 |
"~~/src/HOL/Number_Theory/Primes" |
| 21917 | 19 |
Product_ord |
20 |
SetsAndFunctions |
|
| 31459 | 21 |
Tree |
| 21917 | 22 |
While_Combinator |
23 |
Word |
|
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33042
diff
changeset
|
24 |
"~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" |
| 27421 | 25 |
"~~/src/HOL/ex/Records" |
| 21917 | 26 |
begin |
27 |
||
| 33500 | 28 |
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
29 |
empty: "sublist [] xs" |
|
30 |
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |
|
31 |
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
|
32 |
||
33 |
code_pred sublist . |
|
34 |
||
| 33042 | 35 |
(*avoid popular infix*) |
36 |
code_reserved SML upto |
|
| 31378 | 37 |
|
| 21917 | 38 |
end |