# HG changeset patch
# User berghofe
# Date 1194947619 -3600
# Node ID ddb060d37ca82b817ed2e0cecc4f2963c0cbcf42
# Parent  1d8ebaf5f211a5096e9e2e21e18f5caff0425b32
Tuned.

diff -r 1d8ebaf5f211 -r ddb060d37ca8 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Tue Nov 13 10:50:33 2007 +0100
+++ b/src/HOL/Extraction/Higman.thy	Tue Nov 13 10:53:39 2007 +0100
@@ -7,7 +7,7 @@
 header {* Higman's lemma *}
 
 theory Higman
-imports Main (*"~~/src/HOL/ex/Random"*)
+imports Main
 begin
 
 text {*