| changeset 38117 | 5ae05823cfd9 |
| parent 38116 | 823b1e8bc090 |
| child 38727 | c7f5f0b7dc7f |
| 38116:823b1e8bc090 | 38117:5ae05823cfd9 |
|---|---|
1 theory Code_Prolog_Examples |
1 theory Code_Prolog_Examples |
2 imports Predicate_Compile_Alternative_Defs |
2 imports Code_Prolog |
3 uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" |
|
4 begin |
3 begin |
5 |
4 |
6 section {* Example append *} |
5 section {* Example append *} |
7 |
6 |
8 inductive append |
7 inductive append |