Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
authorchaieb
Tue, 05 Jun 2007 20:46:25 +0200
changeset 23265 a6992b91fdde
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 file | annotate | diff | comparison | revisions 
--- 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
isabelle