proper theory setup for Real/ex/BinEx;
authorwenzelm
Wed Sep 22 21:04:34 1999 +0200 (1999-09-22)
changeset 7577644f9b4ae764
parent 7576 594f09166c38
child 7578 80525697a87c
proper theory setup for Real/ex/BinEx;
src/HOL/IsaMakefile
src/HOL/Real/ex/BinEx.ML
src/HOL/Real/ex/BinEx.thy
src/HOL/Real/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 22 21:02:59 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 22 21:04:34 1999 +0200
     1.3 @@ -90,7 +90,8 @@
     1.4  
     1.5  HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
     1.6  
     1.7 -$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
     1.8 +$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \
     1.9 +  Real/ex/BinEx.thy
    1.10  	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
    1.11  
    1.12  
     2.1 --- a/src/HOL/Real/ex/BinEx.ML	Wed Sep 22 21:02:59 1999 +0200
     2.2 +++ b/src/HOL/Real/ex/BinEx.ML	Wed Sep 22 21:04:34 1999 +0200
     2.3 @@ -11,59 +11,59 @@
     2.4  
     2.5  Goal "(#1359::real)  +  #-2468 = #-1109";
     2.6  by (Simp_tac 1);
     2.7 -result();
     2.8 +qed "";
     2.9  
    2.10  Goal "(#93746::real) +  #-46375 = #47371";
    2.11  by (Simp_tac 1);
    2.12 -result();
    2.13 +qed "";
    2.14  
    2.15  (*** Negation ***)
    2.16  
    2.17  Goal "- (#65745::real) = #-65745";
    2.18  by (Simp_tac 1);
    2.19 -result();
    2.20 +qed "";
    2.21  
    2.22  Goal "- (#-54321::real) = #54321";
    2.23  by (Simp_tac 1);
    2.24 -result();
    2.25 +qed "";
    2.26  
    2.27  
    2.28  (*** Multiplication ***)
    2.29  
    2.30  Goal "(#-84::real)  *  #51 = #-4284";
    2.31  by (Simp_tac 1);
    2.32 -result();
    2.33 +qed "";
    2.34  
    2.35  Goal "(#255::real)  *  #255 = #65025";
    2.36  by (Simp_tac 1);
    2.37 -result();
    2.38 +qed "";
    2.39  
    2.40  Goal "(#1359::real)  *  #-2468 = #-3354012";
    2.41  by (Simp_tac 1);
    2.42 -result();
    2.43 +qed "";
    2.44  
    2.45  (*** Inequalities ***)
    2.46  
    2.47  Goal "(#89::real) * #10 ~= #889";  
    2.48  by (Simp_tac 1); 
    2.49 -result();
    2.50 +qed "";
    2.51  
    2.52  Goal "(#13::real) < #18 - #4";  
    2.53  by (Simp_tac 1); 
    2.54 -result();
    2.55 +qed "";
    2.56  
    2.57  Goal "(#-345::real) < #-242 + #-100";  
    2.58  by (Simp_tac 1); 
    2.59 -result();
    2.60 +qed "";
    2.61  
    2.62  Goal "(#13557456::real) < #18678654";  
    2.63  by (Simp_tac 1); 
    2.64 -result();
    2.65 +qed "";
    2.66  
    2.67  Goal "(#999999::real) <= (#1000001 + #1)-#2";  
    2.68  by (Simp_tac 1); 
    2.69 -result();
    2.70 +qed "";
    2.71  
    2.72  Goal "(#1234567::real) <= #1234567";  
    2.73  by (Simp_tac 1); 
    2.74 -result();
    2.75 +qed "";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/ex/BinEx.thy	Wed Sep 22 21:04:34 1999 +0200
     3.3 @@ -0,0 +1,2 @@
     3.4 +
     3.5 +BinEx = Real
     4.1 --- a/src/HOL/Real/ex/ROOT.ML	Wed Sep 22 21:02:59 1999 +0200
     4.2 +++ b/src/HOL/Real/ex/ROOT.ML	Wed Sep 22 21:04:34 1999 +0200
     4.3 @@ -1,13 +1,13 @@
     4.4 -(*  Title:      HOL/Real/ex/ROOT
     4.5 +(*  Title:      HOL/Real/ex/ROOT.ML
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1999  University of Cambridge
     4.9  
    4.10 -HOL/Real examples
    4.11 +HOL/Real examples.
    4.12  *)
    4.13  
    4.14  writeln "Root file for HOL/Real examples";
    4.15  
    4.16  set proof_timing;
    4.17  
    4.18 -time_use     "BinEx.ML";
    4.19 +time_use_thy "BinEx";