changeset 55447 | aa41ecbdc205 |
parent 54489 | 03ff4d1e6784 |
child 58881 | b9556a055632 |
55446:e77f2858bd59 | 55447:aa41ecbdc205 |
---|---|
4 |
4 |
5 header {* Code generation of prolog programs *} |
5 header {* Code generation of prolog programs *} |
6 |
6 |
7 theory Code_Prolog |
7 theory Code_Prolog |
8 imports Main |
8 imports Main |
9 keywords "values_prolog" :: diag |
|
9 begin |
10 begin |
10 |
11 |
11 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" |
12 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" |
12 |
13 |
13 section {* Setup for Numerals *} |
14 section {* Setup for Numerals *} |