isabelle: src/FOL/thy_data.ML@59bd96046ad6 (annotated)

2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	1	(* Title: FOL/thy_data.ML
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	2	ID: $Id$
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	3	Author: Carsten Clasohm
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	4	Copyright 1995 TU Muenchen
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	5
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	6	Definitions that have to be reread after init_thy_reader has been invoked
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	7	*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	8
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	9	fun simpset_of tname =
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	10	case get_thydata tname "simpset" of
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	11	None => empty_ss
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	12	\| Some (SS_DATA ss) => ss;
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	13
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	14	fun claset_of tname =
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	15	case get_thydata tname "claset" of
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	16	None => empty_cs
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	17	\| Some (CS_DATA cs) => cs;
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	18
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	19

author	wenzelm
	Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754	59bd96046ad6
parent 2469	b50b8c0eec01
permissions	-rw-r--r--