changeset 33615 | 261abc2e3155 |
parent 29921 | 3d50e96bcd6b |
child 35707 | 44936737902d |
33608:5c0024338cef | 33615:261abc2e3155 |
---|---|
1 (* Title: HOLCF/ROOT.ML |
1 (* Title: HOLCF/ROOT.ML |
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
2 Author: Franz Regensburger |
4 |
3 |
5 HOLCF -- a semantic extension of HOL by the LCF logic. |
4 HOLCF -- a semantic extension of HOL by the LCF logic. |
6 *) |
5 *) |
7 |
6 |
8 no_document use_thy "Nat_Int_Bij"; |
7 no_document use_thys ["Nat_Int_Bij"]; |
9 |
8 |
10 use_thy "HOLCF"; |
9 use_thys ["HOLCF"]; |