equal
deleted
inserted
replaced
1 theory Functions imports Main begin |
1 theory Functions imports Main begin |
2 |
|
3 ML "Pretty.margin_default := 64" |
|
4 |
2 |
5 |
3 |
6 text{* |
4 text{* |
7 @{thm[display] id_def[no_vars]} |
5 @{thm[display] id_def[no_vars]} |
8 \rulename{id_def} |
6 \rulename{id_def} |