isabelle: src/HOL/Lambda/ROOT.ML@f24b2818c1e7 (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;
14067 3cc65d66fa12 Added new theories WeakNorm and StrongNorm. berghofe parents: 13550 diff changeset	8	proofs := 2;
3cc65d66fa12 Added new theories WeakNorm and StrongNorm. berghofe parents: 13550 diff changeset	9	IsarOutput.modes := "no_brackets" :: !IsarOutput.modes;
11943 a9672446b45f tuned notation; wenzelm parents: 10264 diff changeset	10
13550 5a176b8dda84 removal of blast.overloaded paulson parents: 13031 diff changeset	11	set timing;
1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	12	time_use_thy "Eta";
13031 3f7824dd8ddf tuned; wenzelm parents: 11943 diff changeset	13	no_document time_use_thy "Accessible_Part";
14067 3cc65d66fa12 Added new theories WeakNorm and StrongNorm. berghofe parents: 13550 diff changeset	14	time_use_thy "StrongNorm";
14090 f24b2818c1e7 Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been berghofe parents: 14067 diff changeset	15	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	16	warning "HOL proof terms required for running theory WeakNorm"
f24b2818c1e7 Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been berghofe parents: 14067 diff changeset	17	else time_use_thy "WeakNorm";

author	berghofe
	Fri, 04 Jul 2003 17:09:26 +0200
changeset 14090	f24b2818c1e7
parent 14067	3cc65d66fa12
child 21676	a45af03f6827
permissions	-rw-r--r--