author | paulson |
Mon, 11 Mar 1996 14:04:37 +0100 | |
changeset 1561 | 9ba6d69f7763 |
parent 1465 | 5d7a7e439cec |
child 1657 | a7a6c3fb3cdd |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/thy_data.ML |
1455
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
1465 | 3 |
Author: Carsten Clasohm |
1455
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; |