author | clasohm |
Mon, 29 Jan 1996 13:48:37 +0100 | |
changeset 1455 | 52a0271621f3 |
child 1465 | 5d7a7e439cec |
permissions | -rw-r--r-- |
1455
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
1 |
(* Title: HOL/thy_data.ML |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
3 |
Author: Carsten Clasohm |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
5 |
|
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
6 |
Definitions that have to be reread after init_thy_reader has been invoked |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
7 |
*) |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
8 |
|
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
9 |
fun simpset_of tname = |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
10 |
case get_thydata (theory_of tname) "simpset" of |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
11 |
None => empty_ss |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
12 |
| Some (SS_DATA ss) => ss; |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
13 |
|
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
14 |
fun datatypes_of tname = |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
15 |
case get_thydata (theory_of tname) "datatypes" of |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
16 |
None => [] |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
17 |
| Some (DT_DATA ds) => ds; |