| changeset 557 | 77ea2de0ca62 |
| parent 538 | e9fd5eff62c1 |
| child 562 | daf404920ab9 |
| 556:3c214b215f7e | 557:77ea2de0ca62 |
|---|---|
1 theory Base |
1 theory Base |
2 imports Main |
2 imports Main |
3 "~~/src/HOL/Library/LaTeXsugar" |
3 "~~/src/HOL/Library/LaTeXsugar" |
4 (*keywords "ML" "setup" "local_setup" :: thy_decl and |
|
5 "ML_prf" :: prf_decl and |
|
6 "ML_val" :: diag |
|
7 *) |
|
8 begin |
4 begin |
9 |
5 |
10 notation (latex output) |
6 notation (latex output) |
11 Cons ("_ # _" [66,65] 65) |
7 Cons ("_ # _" [66,65] 65) |
12 |
8 |