equal
deleted
inserted
replaced
|
1 <?xml version="1.0"?> |
|
2 <!DOCTYPE MODES SYSTEM "catalog.dtd"> |
|
3 |
|
4 <MODES> |
|
5 |
|
6 <MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy" /> |
|
7 <MODE NAME="ml" FILE="ml.xml" FILE_NAME_GLOB="*.ML" /> |
|
8 |
|
9 </MODES> |
|
10 |