isabelle: src/LCF/simpdata.ML@77a1e723151d (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	1	(* Title: LCF/simpdata
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
65 08d3c007ae7c simpdata/basify: now calls new fastype_of lcp parents: 0 diff changeset	4	Copyright 1993 University of Cambridge
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Simplification data for LCF
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
190 4ae10fc91cba deleted harmful basify, which pulled rewrite rules down to base type. nipkow parents: 65 diff changeset	9	val LCF_ss = FOL_ss addsimps
4ae10fc91cba deleted harmful basify, which pulled rewrite rules down to base type. nipkow parents: 65 diff changeset	10	[minimal,
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	11	UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	12	not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	13	not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	14	not_FF_eq_UU,not_FF_eq_TT,
6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	15	COND_UU,COND_TT,COND_FF,
6bcb44e4d6e5 expanded tabs clasohm parents: 190 diff changeset	16	surj_pairing,FST,SND];

author	oheimb
	Tue, 07 Jan 2003 18:08:17 +0100
changeset 13774	77a1e723151d
parent 1461	6bcb44e4d6e5
permissions	-rw-r--r--