| Tue, 21 Aug 2007 00:24:10 +0200 |
wenzelm |
use HOL-ex later;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 17:34:04 +0200 |
huffman |
Word/document/root.tex
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 17:42:38 +0200 |
wenzelm |
converted ex/MT.ML;
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 13:32:28 +0200 |
wenzelm |
make HOL-ex earlier;
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 15:06:58 +0200 |
paulson |
combining the relevance filter with res_atp
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 22:35:40 +0200 |
wenzelm |
reactivated Nominal/Examples/Class.thy;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:18 +0200 |
wenzelm |
added dependency on Tools/Metis/metis.ML;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 15:44:37 +0200 |
wenzelm |
converted Meson tests to proper theory;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 22:21:18 +0200 |
wenzelm |
removed obsolete HOL/Real/ROOT.ML;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:22 +0200 |
wenzelm |
added Tools/lin_arith.ML;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 09:31:23 +0200 |
chaieb |
Added dependency on langford files in Tools/Qelim
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:50 +0200 |
wenzelm |
removed obsolete Tools/res_atpset.ML;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:33:40 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:51:12 +0200 |
obua |
changed sources for HOL-Complex-Matrix
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 10:59:23 +0200 |
berghofe |
Added new package for inductive sets.
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 22:06:49 +0200 |
wenzelm |
HOL-Complex-Matrix: fixed deps -- sort of;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 18:00:57 +0200 |
chaieb |
Dependency on reflection_data.ML to build HOL-ex
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 13:01:48 +0200 |
nipkow |
added NBE
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 12:16:27 +0200 |
krauss |
removed "sum_tools.ML" in favour of BalancedTree
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 17:28:50 +0200 |
wenzelm |
renamed NatSimprocs.thy to Arith_Tools.thy;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:07 +0200 |
wenzelm |
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
|
file |
diff |
annotate
|