isabelle: src/ZF/Coind/Static.ML@f98beaaa7c4f (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 916 diff changeset	1	(* Title: ZF/Coind/Static.ML
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 916 diff changeset	3	Author: Jacob Frost, Cambridge University Computer Laboratory
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5	*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	6
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	7	val elab_constE = ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	9	val elab_varE = ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	10
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	11	val elab_fnE = ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	13	val elab_fixE = ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	14
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	15	val elab_appE = ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	16
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	17	AddSEs [elab_constE, elab_varE, elab_fixE];
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	18
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	19	AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	20
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	21	AddIs [ElabRel.appI];
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	22
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	23	AddEs [elab_appE, elab_fnE];
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	24
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 4091 diff changeset	25	AddDs [ElabRel.dom_subset RS subsetD];

author	wenzelm
	Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282	f98beaaa7c4f
parent 6141	a6922171b396
permissions	-rw-r--r--