isabelle: src/ZF/Coind/Static.thy@f1ad1ed0d110 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Coind/Static.thy
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 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
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	7	Static = BCR +
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: 1478 diff changeset	9	consts ElabRel :: i
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	10
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	11	inductive
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12	domains "ElabRel" <= "TyEnv * Exp * Ty"
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	13	intrs
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	14	constI
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	15	" [\| te:TyEnv; c:Const; t:Ty; isof(c,t) \|] ==>
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	16	<te,e_const(c),t>:ElabRel "
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	17	varI
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	18	" [\| te:TyEnv; x:ExVar; x:te_dom(te) \|] ==>
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	19	<te,e_var(x),te_app(te,x)>:ElabRel "
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	20	fnI
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	21	" [\| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	22	<te_owr(te,x,t1),e,t2>:ElabRel \|] ==>
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	23	<te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	24	fixI
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	25	" [\| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	26	<te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel \|] ==>
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	27	<te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 1478 diff changeset	28	appI
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	29	" [\| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	30	<te,e1,t_fun(t1,t2)>:ElabRel;
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	31	<te,e2,t1>:ElabRel \|] ==>
928a16e02f9f removed \...\ inside strings clasohm parents: 916 diff changeset	32	<te,e_app(e1,e2),t2>:ElabRel "
916 d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	33	type_intrs "te_appI::Exp.intrs@Ty.intrs"
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	34
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	35	end
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	36
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	37
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	38
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	39
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	40
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	41
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	42
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	43
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	44
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	45
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	46
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	47
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	48
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	49
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	50
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	51
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	52
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	53
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	54
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	55
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	56
d03bb9f50b3b New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	57

author	paulson
	Thu, 13 Jul 2000 13:02:20 +0200
changeset 9303	f1ad1ed0d110
parent 6141	a6922171b396
child 11318	6536fb8c9fc6
permissions	-rw-r--r--