| author | wenzelm |
| Fri, 27 Aug 1999 10:49:12 +0200 | |
| changeset 7372 | 79e911c0c7d1 |
| parent 7013 | 8a7fb425e04a |
| child 7373 | 776d888472aa |
| permissions | -rw-r--r-- |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
1 |
(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
3 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
Some rather large datatype examples (from John Harrison). |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
5 |
*) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
6 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
7 |
time_use_thy "Brackin"; |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
8 |
time_use_thy "Instructions"; |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
9 |
time_use_thy "SML"; |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
10 |
time_use_thy "Verilog"; |