proper theory setup for Real/ex/BinEx;

--- a/src/HOL/IsaMakefile	Wed Sep 22 21:02:59 1999 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 22 21:04:34 1999 +0200
@@ -90,7 +90,8 @@
 
 HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
 
-$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
+$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \
+  Real/ex/BinEx.thy
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
 
 

--- a/src/HOL/Real/ex/BinEx.ML	Wed Sep 22 21:02:59 1999 +0200
+++ b/src/HOL/Real/ex/BinEx.ML	Wed Sep 22 21:04:34 1999 +0200
@@ -11,59 +11,59 @@
 
 Goal "(#1359::real)  +  #-2468 = #-1109";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "(#93746::real) +  #-46375 = #47371";
 by (Simp_tac 1);
-result();
+qed "";
 
 (*** Negation ***)
 
 Goal "- (#65745::real) = #-65745";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "- (#-54321::real) = #54321";
 by (Simp_tac 1);
-result();
+qed "";
 
 
 (*** Multiplication ***)
 
 Goal "(#-84::real)  *  #51 = #-4284";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "(#255::real)  *  #255 = #65025";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "(#1359::real)  *  #-2468 = #-3354012";
 by (Simp_tac 1);
-result();
+qed "";
 
 (*** Inequalities ***)
 
 Goal "(#89::real) * #10 ~= #889";  
 by (Simp_tac 1); 
-result();
+qed "";
 
 Goal "(#13::real) < #18 - #4";  
 by (Simp_tac 1); 
-result();
+qed "";
 
 Goal "(#-345::real) < #-242 + #-100";  
 by (Simp_tac 1); 
-result();
+qed "";
 
 Goal "(#13557456::real) < #18678654";  
 by (Simp_tac 1); 
-result();
+qed "";
 
 Goal "(#999999::real) <= (#1000001 + #1)-#2";  
 by (Simp_tac 1); 
-result();
+qed "";
 
 Goal "(#1234567::real) <= #1234567";  
 by (Simp_tac 1); 
-result();
+qed "";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ex/BinEx.thy	Wed Sep 22 21:04:34 1999 +0200
@@ -0,0 +1,2 @@
+
+BinEx = Real

--- a/src/HOL/Real/ex/ROOT.ML	Wed Sep 22 21:02:59 1999 +0200
+++ b/src/HOL/Real/ex/ROOT.ML	Wed Sep 22 21:04:34 1999 +0200
@@ -1,13 +1,13 @@
-(*  Title:      HOL/Real/ex/ROOT
+(*  Title:      HOL/Real/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 
-HOL/Real examples
+HOL/Real examples.
 *)
 
 writeln "Root file for HOL/Real examples";
 
 set proof_timing;
 
-time_use     "BinEx.ML";
+time_use_thy "BinEx";