| changeset 22823 | fa9ff469247f | 
| parent 22448 | f982e73e36de | 
| child 23098 | 11e1a67fbfe8 | 
| 22822:c1a6a2159e69 | 22823:fa9ff469247f | 
|---|---|
| 4 | 4 | 
| 5 Various examples involving nominal datatypes. | 5 Various examples involving nominal datatypes. | 
| 6 *) | 6 *) | 
| 7 | 7 | 
| 8 use_thy "CR"; | 8 use_thy "CR"; | 
| 9 use_thy "CR_Takahashi"; | |
| 9 use_thy "Class"; | 10 use_thy "Class"; | 
| 10 use_thy "Compile"; | 11 use_thy "Compile"; | 
| 11 use_thy "Fsub"; | 12 use_thy "Fsub"; | 
| 12 use_thy "Height"; | 13 use_thy "Height"; | 
| 13 use_thy "Lambda_mu"; | 14 use_thy "Lambda_mu"; |