equal
deleted
inserted
replaced
1 (* the problems and methods as stored in hierarchies |
1 (* the problems and methods as stored in hierarchies |
2 author Walther Neuper 1998, Mathias Lehnfeld |
2 author Walther Neuper 1998, Mathias Lehnfeld |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 |
|
5 use"ME/ptyps.sml"; |
|
6 use"ptyps.sml"; |
|
7 *) |
4 *) |
8 |
5 |
9 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) |
6 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) |
10 val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script})) |
7 val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script})) |
11 "unknown::'a => unknow"; |
8 "unknown::'a => unknow"; |