# HG changeset patch
# User wenzelm
# Date 979294086 -3600
# Node ID e12892e4666a4e02bdab24b3194aa5f4bf7bc126
# Parent  1715cb1472941132456f054688e2f0b0c527bdc8
added Sigma_Algebra;

diff -r 1715cb147294 -r e12892e4666a src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Fri Jan 12 11:06:50 2001 +0100
+++ b/src/HOL/Induct/ROOT.ML	Fri Jan 12 11:08:06 2001 +0100
@@ -3,6 +3,7 @@
 Examples of Inductive and Coinductive Definitions.
 *)
 
+time_use_thy "Sigma_Algebra";
 time_use_thy "Perm";
 time_use_thy "Comb";
 time_use_thy "Mutil";