| 2009-02-12 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
|
| 2009-02-11 |
nipkow |
Moved Order_Relation into Library and moved some of it into Relation.
|
file |
diff |
annotate
|
| 2009-02-09 |
chaieb |
added Determinants to Library
|
file |
diff |
annotate
|
| 2009-02-09 |
chaieb |
added Euclidean_Space and Glbs to Library
|
file |
diff |
annotate
|
| 2009-02-09 |
chaieb |
Added HOL/Library/Finite_Cartesian_Product.thy to Library
|
file |
diff |
annotate
|
| 2009-02-06 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| 2009-02-06 |
chaieb |
fixed dependencies : Theory Dense_Linear_Order moved to Library
|
file |
diff |
annotate
|
| 2009-02-05 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-02-05 |
haftmann |
moved Random.thy to Library
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Add approximation method
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Added new Float theory and moved old Library/Float.thy to ComputeFloat
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
merged Big0
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
established session HOL-Reflection
|
file |
diff |
annotate
|
| 2009-02-16 |
wenzelm |
removed obsolete axclass manual and examples;
|
file |
diff |
annotate
|
| 2009-02-02 |
haftmann |
added Mapping.thy to Library
|
file |
diff |
annotate
|
| 2009-01-30 |
krauss |
fixed case
|
file |
diff |
annotate
|
| 2009-01-30 |
chaieb |
Added Formal_Power_Series_Examples to HOL-ex image
|
file |
diff |
annotate
|
| 2009-01-29 |
chaieb |
Inserted Formal_Power_Series.thy under Library
|
file |
diff |
annotate
|
| 2009-01-28 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| 2009-01-26 |
haftmann |
entry point for Word library now named Word
|
file |
diff |
annotate
|
| 2009-01-17 |
haftmann |
no document for HOL-Base
|
file |
diff |
annotate
|
| 2009-01-16 |
haftmann |
added HOL-Base image
|
file |
diff |
annotate
|
| 2009-01-13 |
huffman |
add Polynomial.thy to makefile
|
file |
diff |
annotate
|
| 2009-01-08 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
file |
diff |
annotate
|
| 2008-12-29 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| 2008-12-27 |
krauss |
renamed LexOrds.thy to Termination.thy; examples for sizechange method
|
file |
diff |
annotate
|
| 2008-12-16 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| 2008-12-15 |
nipkow |
merged
|
file |
diff |
annotate
|
| 2008-12-11 |
nipkow |
Testfile for Stefan's code generator
|
file |
diff |
annotate
|
| 2008-12-15 |
haftmann |
moved value.ML to src/Tools
|
file |
diff |
annotate
|
| 2008-12-10 |
nipkow |
moved ContNotDenum into Library
|
file |
diff |
annotate
|
| 2008-12-03 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| 2008-11-29 |
nipkow |
new file float_syntax.ML
|
file |
diff |
annotate
|
| 2008-11-17 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
file |
diff |
annotate
|
| 2008-11-15 |
wenzelm |
clean: added HOL-Main;
|
file |
diff |
annotate
|
| 2008-11-13 |
haftmann |
moved assert to Heap_Monad.thy
|
file |
diff |
annotate
|
| 2008-10-21 |
berghofe |
Added nominal_inductive2.ML
|
file |
diff |
annotate
|
| 2008-10-17 |
wenzelm |
reactivated HOL-Matrix;
|
file |
diff |
annotate
|
| 2008-10-16 |
ballarin |
Removed ex/Locales.thy.
|
file |
diff |
annotate
|
| 2008-10-14 |
wenzelm |
renamed AtpThread to AtpWrapper;
|
file |
diff |
annotate
|
| 2008-10-04 |
wenzelm |
replaced ISATOOL by ISABELLE_TOOL;
|
file |
diff |
annotate
|
| 2008-10-03 |
wenzelm |
version of sledgehammer using threads instead of processes, misc cleanup;
|
file |
diff |
annotate
|
| 2008-10-03 |
wenzelm |
removed old/unused setup of raw ATP oracles;
|
file |
diff |
annotate
|
| 2008-09-29 |
haftmann |
separate HOL-Main image
|
file |
diff |
annotate
|
| 2008-09-28 |
wenzelm |
HOL no longer depends on HOL-Plain;
|
file |
diff |
annotate
|
| 2008-09-27 |
wenzelm |
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
|
file |
diff |
annotate
|
| 2008-09-22 |
berghofe |
Added coherent logic prover.
|
file |
diff |
annotate
|
| 2008-09-22 |
haftmann |
different session branches for HOL-Plain vs. Plain
|
file |
diff |
annotate
|
| 2008-09-16 |
haftmann |
moved term_of syntax to separate theory
|
file |
diff |
annotate
|
| 2008-09-16 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| 2008-09-03 |
nipkow |
removed ex/Puzzle
|
file |
diff |
annotate
|
| 2008-09-02 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| 2008-08-28 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| 2008-08-27 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|
| 2008-08-05 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
file |
diff |
annotate
|
| 2008-08-01 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| 2008-07-30 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| 2008-07-29 |
ballarin |
New theory on divisibility;
|
file |
diff |
annotate
|
| 2008-07-29 |
haftmann |
corrected Pure dependency
|
file |
diff |
annotate
|
| 2008-07-25 |
haftmann |
tuned
|
file |
diff |
annotate
|