# HG changeset patch
# User paulson
# Date 936019516 -7200
# Node ID 4137c951b36bc852271405b6a58d04b6407872c2
# Parent  b7ca64c8fa64a4cd7bcfc6caf48e13f8db75f0b0
new directory HOL/Real/ex of real examples

diff -r b7ca64c8fa64 -r 4137c951b36b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Aug 30 14:11:47 1999 +0200
+++ b/src/HOL/IsaMakefile	Mon Aug 30 15:25:16 1999 +0200
@@ -11,8 +11,8 @@
 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
   HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
-  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
-  TLA-Buffer TLA-Memory
+  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-Ex \
+  TLA-Inc TLA-Buffer TLA-Memory
 
 all: images test
 
@@ -85,6 +85,11 @@
   Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
+## HOL-Real-Ex
+
+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
 
 ## HOL-Subst
 
diff -r b7ca64c8fa64 -r 4137c951b36b src/HOL/Real/ex/BinEx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ex/BinEx.ML	Mon Aug 30 15:25:16 1999 +0200
@@ -0,0 +1,69 @@
+(*  Title:      HOL/Real/ex/BinEx.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+Examples of performing binary arithmetic by simplification
+This time we use the reals, though the representation is just of integers.
+*)
+
+(*** Addition ***)
+
+Goal "(#1359::real)  +  #-2468 = #-1109";
+by (Simp_tac 1);
+result();
+
+Goal "(#93746::real) +  #-46375 = #47371";
+by (Simp_tac 1);
+result();
+
+(*** Negation ***)
+
+Goal "- (#65745::real) = #-65745";
+by (Simp_tac 1);
+result();
+
+Goal "- (#-54321::real) = #54321";
+by (Simp_tac 1);
+result();
+
+
+(*** Multiplication ***)
+
+Goal "(#-84::real)  *  #51 = #-4284";
+by (Simp_tac 1);
+result();
+
+Goal "(#255::real)  *  #255 = #65025";
+by (Simp_tac 1);
+result();
+
+Goal "(#1359::real)  *  #-2468 = #-3354012";
+by (Simp_tac 1);
+result();
+
+(*** Inequalities ***)
+
+Goal "(#89::real) * #10 ~= #889";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#13::real) < #18 - #4";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#-345::real) < #-242 + #-100";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#13557456::real) < #18678654";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#999999::real) <= (#1000001 + #1)-#2";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#1234567::real) <= #1234567";  
+by (Simp_tac 1); 
+result();
diff -r b7ca64c8fa64 -r 4137c951b36b src/HOL/Real/ex/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 15:25:16 1999 +0200
@@ -0,0 +1,12 @@
+(*  Title:      HOL/Real/ex/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+HOL/Real examples
+*)
+
+writeln "Root file for HOL/Real examples";
+
+set proof_timing;
+