isabelle: src/HOL/Induct/ROOT.ML@ae42b36a50c2 (annotated)

3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	1	(* Title: HOL/Induct/ROOT
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	2	ID: $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	4	Copyright 1997 University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	5
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4449 diff changeset	6	Examples of Inductive and Coinductive Definitions
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	7	*)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	8
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	10
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	11	writeln"Root file for HOL/Induct";
4449 df30e75f670f tuned; wenzelm parents: 3120 diff changeset	12	set proof_timing;
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	13	time_use_thy "Perm";
5417 1f533238b53b new theory Induct/FoldSet paulson parents: 5078 diff changeset	14	time_use_thy "FoldSet";
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	15	time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	16	time_use_thy "Mutil";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	17	time_use_thy "Acc";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	18	time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	19	time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	20	time_use_thy "LFilter";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	21	time_use_thy "Term";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	22	time_use_thy "Simult";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	23	time_use_thy "Exp";

author	oheimb
	Thu, 24 Sep 1998 17:17:14 +0200
changeset 5553	ae42b36a50c2
parent 5417	1f533238b53b
child 5616	497eeeace3fc
permissions	-rw-r--r--