isabelle: src/HOL/Lambda/ROOT.ML@4d51ddd6aa5c (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/Lambda/ROOT.ML
1126 50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow
5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: 1465 diff changeset	4	Copyright 1998 TUM
1126 50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	5	*)
50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	6
11943 a9672446b45f tuned notation; wenzelm parents: 10264 diff changeset	7	Syntax.ambiguity_level := 100;
25374 7657a081fcb4 qualified Proofterm.proofs; wenzelm parents: 24994 diff changeset	8	Proofterm.proofs := 2;
11943 a9672446b45f tuned notation; wenzelm parents: 10264 diff changeset	9
26748 4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy krauss parents: 25374 diff changeset	10	no_document use_thys ["Code_Integer"];
24535 d458d44639fc Added Standardization theory. berghofe parents: 24156 diff changeset	11	use_thys ["Eta", "StrongNorm", "Standardization"];
14090 f24b2818c1e7 Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been berghofe parents: 14067 diff changeset	12	if HOL_proofs < 2 then
f24b2818c1e7 Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been berghofe parents: 14067 diff changeset	13	warning "HOL proof terms required for running theory WeakNorm"
21676 a45af03f6827 no timing; wenzelm parents: 14090 diff changeset	14	else use_thy "WeakNorm";

author	krauss
	Fri, 25 Apr 2008 15:30:33 +0200
changeset 26748	4d51ddd6aa5c
parent 25374	7657a081fcb4
child 33615	261abc2e3155
permissions	-rw-r--r--