Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
authorchaieb
Tue Jun 05 20:46:25 2007 +0200 (2007-06-05)
changeset 23265a6992b91fdde
parent 23264 324622260d29
child 23266 50f0a4f12ed3
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 05 20:44:12 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 05 20:46:25 2007 +0200
     1.3 @@ -191,7 +191,9 @@
     1.4    Complex/ex/ROOT.ML Complex/ex/document/root.tex \
     1.5    Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
     1.6    Complex/ex/Ferrante_Rackoff_Ex.thy \
     1.7 -  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
     1.8 +  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
     1.9 +  Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
    1.10 +  Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
    1.11  	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
    1.12  
    1.13