isabelle: src/ZF/Resid/ROOT.ML@a79d4683fadf (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: ZF/Resid/ROOT
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	6	Executes the Residuals example.
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	7	This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus.
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	8
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9	By Ole Rasmussen, following the Coq proof given in
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	10
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	11	G�rard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	J. Functional Programming 4(3) 1994, 371-394.
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	13	*)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	14
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 4446 diff changeset	15	writeln"Root file for ZF/Resid";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	16
4446 097004a470fb tuned; wenzelm parents: 3733 diff changeset	17	set proof_timing;
3733 1baedb1d4627 Previously loaded the WRONG THEORY, ignoring Confluence... paulson parents: 1461 diff changeset	18	time_use_thy "Conversion";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	writeln"END: Root file for ZF/Resid";

author	wenzelm
	Thu, 26 Aug 1999 19:01:58 +0200
changeset 7367	a79d4683fadf
parent 6349	f7750d816c21
child 9000	c20d58286a51
permissions	-rw-r--r--