2014-08-19 |
Andreas Lochbihler |
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
|
file |
diff |
annotate
|
2014-08-19 |
blanchet |
avoid old 'smt' method in examples
|
file |
diff |
annotate
|
2014-07-24 |
wenzelm |
proper scope of comments;
|
file |
diff |
annotate
|
2014-07-21 |
traytel |
regression test for datatypes defined in IsaFoR
|
file |
diff |
annotate
|
2014-07-20 |
wenzelm |
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
|
file |
diff |
annotate
|
2014-07-11 |
Andreas Lochbihler |
reactivate session Quickcheck_Examples
|
file |
diff |
annotate
|
2014-07-11 |
Andreas Lochbihler |
adapt and reactivate Quickcheck_Types and add two test cases
|
file |
diff |
annotate
|
2014-07-04 |
wenzelm |
revived unchecked theory (see cebaf814ca6e);
|
file |
diff |
annotate
|
2014-06-29 |
blanchet |
use SMT2
|
file |
diff |
annotate
|
2014-05-22 |
wenzelm |
include Nominal2 keywords -- Proof General legacy;
|
file |
diff |
annotate
|
2014-05-19 |
hoelzl |
fixed document generation for HOL-Probability
|
file |
diff |
annotate
|
2014-05-11 |
webertj |
Replaced refute with nitpick.
|
file |
diff |
annotate
|
2014-05-09 |
haftmann |
removed junk from library theory
|
file |
diff |
annotate
|
2014-05-01 |
boehmes |
use SMT2 for Boogie examples
|
file |
diff |
annotate
|
2014-05-01 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
2014-04-30 |
wenzelm |
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
|
file |
diff |
annotate
|
2014-04-29 |
wenzelm |
systematic replacement of 'files' by 'document_files';
|
file |
diff |
annotate
|
2014-04-24 |
haftmann |
now covered by AFP 3ddac3e572cf
|
file |
diff |
annotate
|
2014-04-23 |
kuncar |
all BNF tests can be part of a normal session because they are much faster now
|
file |
diff |
annotate
|
2014-04-08 |
blanchet |
added 'datatype_compat' examples/tests
|
file |
diff |
annotate
|
2014-03-19 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
2014-03-13 |
blanchet |
use 'smt2' in SMT examples as much as currently possible
|
file |
diff |
annotate
|
2014-03-07 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
2014-02-24 |
paulson |
Gauss.thy ported from Old_Number_Theory (unfinished)
|
file |
diff |
annotate
|
2014-02-21 |
wenzelm |
more standard theory name;
|
file |
diff |
annotate
|
2014-02-19 |
haftmann |
offical tool
|
file |
diff |
annotate
|
2014-02-19 |
sultana |
reconstruction framework for LEO-II's TPTP proofs;
|
file |
diff |
annotate
|
2014-02-13 |
wenzelm |
reactivate some examples that still appear to work;
|
file |
diff |
annotate
|
2014-02-13 |
wenzelm |
do not redefine outer syntax commands;
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
2014-02-09 |
wenzelm |
minimal document;
|
file |
diff |
annotate
|
2014-02-04 |
paulson |
Restoration of Pocklington.thy. Tidying.
|
file |
diff |
annotate
|
2014-02-01 |
wenzelm |
proper config options;
|
file |
diff |
annotate
|
2014-01-29 |
paulson |
Replacing the theory Library/Binomial by Number_Theory/Binomial
|
file |
diff |
annotate
|
2014-01-23 |
wenzelm |
no document for Cartouche_Examples: avoid problems typesetting "\001";
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
dissolved BNF session
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
minimized Nitpick's dependencies
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
moved BNF examples
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
killed obsolete session
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
|
file |
diff |
annotate
|
2014-01-18 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
2014-01-16 |
blanchet |
moved 'Zorn' into 'Main', since it's a BNF dependency
|
file |
diff |
annotate
|
2014-01-10 |
traytel |
new codatatype example: stream processors
|
file |
diff |
annotate
|
2013-11-18 |
blanchet |
compile
|
file |
diff |
annotate
|
2013-11-18 |
blanchet |
split 'Cardinal_Arithmetic' 3-way
|
file |
diff |
annotate
|
2013-11-18 |
blanchet |
started three-way split of 'HOL-Cardinals'
|
file |
diff |
annotate
|
2013-11-16 |
wenzelm |
merged
|
file |
diff |
annotate
|
2013-11-16 |
wenzelm |
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
|
file |
diff |
annotate
|
2013-11-14 |
haftmann |
explicit inclusion of data refinement theory into HOL-Library session
|
file |
diff |
annotate
|
2013-10-23 |
blanchet |
added 'primcorec' examples
|
file |
diff |
annotate
|
2013-09-26 |
wenzelm |
added Isabelle/ML example;
|
file |
diff |
annotate
|
2013-09-23 |
blanchet |
register codatatypes with Nitpick
|
file |
diff |
annotate
|
2013-09-17 |
kuncar |
include Int_Pow into Quotient_Examples; add end of the theory
|
file |
diff |
annotate
|
2013-09-06 |
noschinl |
added examples for Simps_Case_Conv
|
file |
diff |
annotate
|
2013-08-30 |
blanchet |
added example
|
file |
diff |
annotate
|
2013-08-23 |
wenzelm |
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
|
file |
diff |
annotate
|
2013-08-21 |
blanchet |
renamed theory files to be closer to (new) command names
|
file |
diff |
annotate
|
2013-07-24 |
nipkow |
merged Def_Init_Sound_X into Def_Init_X
|
file |
diff |
annotate
|
2013-07-23 |
boehmes |
removed obsolete HOL-Boogie session;
|
file |
diff |
annotate
|
2013-07-02 |
wenzelm |
clarified Proofterm.proofs vs. Goal.skip_proofs;
|
file |
diff |
annotate
|