| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:34 +0200 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:38 +0200 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 06:21:40 +0200 |
nipkow |
sorting
|
file |
diff |
annotate
|
| Sun, 16 Sep 2007 21:04:44 +0200 |
wenzelm |
added Induct/Common_Patterns.thy;
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 11:52:13 +0200 |
berghofe |
- New theories Lambda/NormalForm and Lambda/Standardization
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 13:58:00 +0200 |
wenzelm |
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 11:10:28 +0200 |
wenzelm |
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:24:34 +0200 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 03:56:24 +0200 |
huffman |
HOL-Word-Examples
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 16:47:16 +0200 |
huffman |
Word/BinInduct.thy
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 21:09:21 +0200 |
huffman |
removed Word/Size.thy;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 16:54:43 +0200 |
huffman |
Word/WordBoolList.thy
|
file |
diff |
annotate
|
| 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
|