isabelle: src/Sequents/LK/ROOT.ML@b76a26835a5c (annotated)

6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	1	(* Title: LK/ex/ROOT
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	2	ID: $Id$
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	4	Copyright 1992 University of Cambridge
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	5
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6	Executes all examples for Classical Logic.
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	7	*)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	8
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	9	writeln"Root file for LK examples";
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	10
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	11	set proof_timing;
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	12	time_use "prop.ML";
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	13	time_use "quant.ML";
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	14	time_use "hardquant.ML";
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: 6349 diff changeset	15	use_thy "Nat";

author	paulson
	Tue, 27 Jul 1999 18:50:14 +0200
changeset 7091	b76a26835a5c
parent 6349	f7750d816c21
child 9000	c20d58286a51
permissions	-rw-r--r--