# HG changeset patch
# User bulwahn
# Date 1330157271 -3600
# Node ID 34e26d5119ef3c90fb6ded6d9219079600e953bf
# Parent  3fc49e6998dae92c3a7d963155a64e97b43ae87a
adding some more test invocations of find_unused_assms

diff -r 3fc49e6998da -r 34e26d5119ef src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy	Sat Feb 25 09:07:43 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy	Sat Feb 25 09:07:51 2012 +0100
@@ -1,5 +1,5 @@
 theory Find_Unused_Assms_Examples
-imports Main
+imports Complex_Main
 begin
 
 section {* Arithmetics *}
@@ -8,7 +8,8 @@
 
 find_unused_assms Divides
 find_unused_assms GCD
-find_unused_assms MacLaurin
+find_unused_assms RealDef
+find_unused_assms RComplete
 
 section {* Set Theory *}