| 2009-10-28 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| 2009-10-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2009-10-28 |
paulson |
merged
|
file |
diff |
annotate
|
| 2009-10-28 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
| 2009-10-27 |
paulson |
merged
|
file |
diff |
annotate
|
| 2009-10-27 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|
| 2009-10-27 |
bulwahn |
merged
|
file |
diff |
annotate
|
| 2009-10-27 |
bulwahn |
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
|
file |
diff |
annotate
|
| 2009-10-27 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|
| 2009-10-27 |
boehmes |
removed unused file smt_builtin.ML,
|
file |
diff |
annotate
|
| 2009-10-26 |
wenzelm |
recovered sort indentation for "sort position", as documented in the file;
|
file |
diff |
annotate
|
| 2009-10-26 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2009-10-26 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2009-10-26 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2009-10-23 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|
| 2009-10-22 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|
| 2009-10-26 |
berghofe |
merged
|
file |
diff |
annotate
|
| 2009-10-26 |
berghofe |
Added Pattern.thy to Nominal/Examples.
|
file |
diff |
annotate
|
| 2009-10-26 |
wenzelm |
more precise dependencies, notably for HOL-Multivariate_Analysis;
|
file |
diff |
annotate
|
| 2009-10-26 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-10-23 |
himmelma |
distinguished session for multivariate analysis
|
file |
diff |
annotate
|
| 2009-10-23 |
krauss |
renamed auto_term.ML -> relation.ML
|
file |
diff |
annotate
|
| 2009-10-23 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| 2009-10-23 |
krauss |
renamed FundefDatatype -> Function_Fun
|
file |
diff |
annotate
|
| 2009-10-23 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-10-23 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
| 2009-10-23 |
krauss |
pat_completeness gets its own file
|
file |
diff |
annotate
|
| 2009-10-20 |
wenzelm |
modernized session SET_Protocol;
|
file |
diff |
annotate
|
| 2009-10-20 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
|
| 2009-10-20 |
wenzelm |
modernized session Isar_Examples;
|
file |
diff |
annotate
|
| 2009-10-20 |
wenzelm |
more accurate dependencies for HOL-SMT, which is a session with image;
|
file |
diff |
annotate
|
| 2009-10-20 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
| 2009-10-01 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| 2009-09-28 |
wenzelm |
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
|
file |
diff |
annotate
|
| 2009-09-24 |
bulwahn |
merged; adopted to changes from Code_Evaluation in the predicate compiler
|
file |
diff |
annotate
|
| 2009-09-23 |
bulwahn |
moved predicate compiler to Tools
|
file |
diff |
annotate
|
| 2009-09-23 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
| 2009-09-23 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
added session theory for Bali and Nominal_Examples
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
added session entry point theories
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
entry point theory for examples; reactivated half-dead example
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
theory entry point for session Hoare_Parallel (now also with proper underscore)
|
file |
diff |
annotate
|
| 2009-09-18 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|
| 2009-09-10 |
haftmann |
obey underscore naming convention
|
file |
diff |
annotate
|
| 2009-09-10 |
haftmann |
generic transfer procedure
|
file |
diff |
annotate
|
| 2009-09-04 |
boehmes |
tuned
|
file |
diff |
annotate
|
| 2009-09-02 |
boehmes |
merged
|
file |
diff |
annotate
|
| 2009-09-02 |
boehmes |
moved Mirabelle from HOL/Tools to HOL,
|
file |
diff |
annotate
|
| 2009-09-02 |
wenzelm |
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
|
file |
diff |
annotate
|
| 2009-09-01 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| 2009-08-26 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
| 2009-08-21 |
krauss |
fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
|
file |
diff |
annotate
|
| 2009-08-06 |
wenzelm |
misc changes to SOS by Philipp Meyer:
|
file |
diff |
annotate
|
| 2009-08-04 |
wenzelm |
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
|
file |
diff |
annotate
|
| 2009-07-31 |
boehmes |
added Mirabelle
|
file |
diff |
annotate
|
| 2009-07-23 |
chaieb |
merged
|
file |
diff |
annotate
|
| 2009-07-15 |
chaieb |
Moved important theorems from FPS_Examples to FPS --- they are not
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| 2009-07-10 |
krauss |
move Kleene_Algebra to Library
|
file |
diff |
annotate
|
| 2009-07-03 |
haftmann |
nominal.ML is nominal_datatype.ML
|
file |
diff |
annotate
|