# HG changeset patch
# User chaieb
# Date 1181069185 -7200
# Node ID a6992b91fdde734b1e918cb668cb7f3237b9a6b8
# Parent  324622260d2937ab0504cf39a803bafa3c1e018e
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic

diff -r 324622260d29 -r a6992b91fdde src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 05 20:44:12 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 05 20:46:25 2007 +0200
@@ -191,7 +191,9 @@
   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
   Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
   Complex/ex/Ferrante_Rackoff_Ex.thy \
-  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
+  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
+  Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
+  Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex