isabelle: src/HOL/thy_data.ML@64ee96ebf32a (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1455 diff changeset	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 5d7a7e439cec expanded tabs clasohm parents: 1455 diff changeset	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;

author	berghofe
	Thu, 28 Mar 1996 17:21:58 +0100
changeset 1627	64ee96ebf32a
parent 1465	5d7a7e439cec
child 1657	a7a6c3fb3cdd
permissions	-rw-r--r--