equal
deleted
inserted
replaced
10 "~~/src/HOL/Library/Code_Target_Int" |
10 "~~/src/HOL/Library/Code_Target_Int" |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Formalization by Stefan Berghofer. Partly based on a paper proof by |
14 Formalization by Stefan Berghofer. Partly based on a paper proof by |
15 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
15 Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}. |
16 *} |
16 *} |
17 |
17 |
18 |
18 |
19 subsection {* Main theorems *} |
19 subsection {* Main theorems *} |
20 |
20 |