isabelle: src/ZF/Resid/Redex.thy@a5839ecee7b8 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: Redex.thy
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Ole Rasmussen
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	5	Logic Image: ZF
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	6	*)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	7
2874 b1e7e2179597 Datatype declarations now require theory Datatype--NOT in quotes paulson parents: 1478 diff changeset	8	Redex = Datatype +
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	10	redexes :: i
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	11
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	datatype
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	13	"redexes" = Var ("n: nat")
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	14	\| Fun ("t: redexes")
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15	\| App ("b:bool" ,"f:redexes" , "a:redexes")
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	16	type_intrs "[bool_into_univ]"
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	17
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	22	defs
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	23	redex_rec_def
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 1048 diff changeset	24	"redex_rec(p,b,c,d) ==
3840 e0baea4d485a fixed dots; wenzelm parents: 2874 diff changeset	25	Vrec(p, %p g. redexes_case(b, %x. c(x,g`x),
e0baea4d485a fixed dots; wenzelm parents: 2874 diff changeset	26	%n x y. d(n, x, y, g`x, g`y), p))"
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	27	end
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	28

author	wenzelm
	Wed, 15 Oct 1997 15:12:59 +0200
changeset 3872	a5839ecee7b8
parent 3840	e0baea4d485a
child 6046	2c8a8be36c94
permissions	-rw-r--r--