| Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 18:10:23 -0700 |
huffman |
add Multivariate_Analysis dependencies
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:10:24 +0200 |
haftmann |
avoid case-sensitive name for example theory
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 14:32:48 -0700 |
huffman |
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 13:14:20 +0200 |
wenzelm |
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 09:41:21 +0200 |
krauss |
removed obsolete recdef-related examples
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:12:36 +0200 |
wenzelm |
moved old code generator to src/Tools/;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 09:05:21 +0200 |
blanchet |
load lambda-lifting structure earlier, so it can be used in Metis
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 11:52:57 +0200 |
krauss |
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Mon, 01 Aug 2011 09:31:10 -0700 |
huffman |
new theory HOL/Library/Product_Lattice.thy
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 18:11:38 +0200 |
bulwahn |
more precise dependencies
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 10:43:14 +0200 |
bulwahn |
removing SML_Quickcheck
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 13:29:54 +0200 |
boehmes |
more precise dependencies
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 13:27:01 +0200 |
boehmes |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 09:23:09 +0200 |
boehmes |
removed old (unused) SMT monomorphizer
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 10:48:00 +0200 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:35:44 +0200 |
hoelzl |
rename Nat_Infinity (inat) to Extended_Nat (enat)
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 10:11:08 +0200 |
Cezary Kaliszyk |
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 08:46:17 +0200 |
kleing |
build an image for HOL-IMP
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 22:08:11 +0200 |
krauss |
added missing dependencies;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
cleanly separate TPTP related files from other examples
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 15:50:45 +0200 |
krauss |
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
moved ATP dependencies to HOL-Plain, where they belong
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 11:26:02 +0200 |
bulwahn |
improving actual dependencies
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 09:42:46 +0200 |
hoelzl |
move conditional expectation to its own theory file
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 13:30:28 -0700 |
huffman |
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
|
file |
diff |
annotate
|
| Fri, 17 Jun 2011 20:38:43 +0200 |
kleing |
IMP compiler with int, added reverse soundness direction
|
file |
diff |
annotate
|