| 2020-07-17 |
wenzelm |
proper session imports;
|
file |
diff |
annotate
|
| 2020-07-16 |
wenzelm |
proper import sessions;
|
file |
diff |
annotate
|
| 2020-07-13 |
wenzelm |
clarified examples;
|
file |
diff |
annotate
|
| 2020-07-02 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| 2020-06-09 |
paulson |
New Ackermann development
|
file |
diff |
annotate
|
| 2020-06-08 |
wenzelm |
clarified sessions;
|
file |
diff |
annotate
|
| 2020-06-08 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/HOL";
|
file |
diff |
annotate
|
| 2020-06-08 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/Pure";
|
file |
diff |
annotate
|
| 2020-05-17 |
nipkow |
another AVL tree version
|
file |
diff |
annotate
|
| 2020-05-04 |
Manuel Eberl |
New HOL simproc 'datatype_no_proper_subterm'
|
file |
diff |
annotate
|
| 2020-05-12 |
wenzelm |
clarified session imports: avoid bulky HOL-Library image;
|
file |
diff |
annotate
|
| 2020-05-04 |
nipkow |
AVL trees with balance tags
|
file |
diff |
annotate
|
| 2020-04-25 |
nipkow |
added Height_Balanced_Trees
|
file |
diff |
annotate
|
| 2020-04-17 |
paulson |
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
|
file |
diff |
annotate
|
| 2020-03-03 |
haftmann |
library theory for extractions of equations x = t into premises
|
file |
diff |
annotate
|
| 2020-02-28 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| 2020-02-03 |
nipkow |
added Interval_Tree.thy
|
file |
diff |
annotate
|
| 2020-01-19 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| 2020-01-07 |
nipkow |
alternative deletion in Red-Black trees
|
file |
diff |
annotate
|
| 2019-12-10 |
traytel |
an extensive example for lift_bnf across quotients
|
file |
diff |
annotate
|
| 2019-11-30 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| 2019-11-04 |
haftmann |
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
|
file |
diff |
annotate
|
| 2019-10-28 |
immler |
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| 2019-10-28 |
immler |
added examples for "metric" method, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| 2019-10-13 |
wenzelm |
clarified sessions/directories;
|
file |
diff |
annotate
|
| 2019-10-07 |
wenzelm |
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
|
file |
diff |
annotate
|
| 2019-10-02 |
wenzelm |
just one dump_checkpoint Main -- potentially more robust;
|
file |
diff |
annotate
|
| 2019-09-08 |
wenzelm |
clarified syntax: 'directories' and 'theories' belong together;
|
file |
diff |
annotate
|
| 2019-09-08 |
wenzelm |
declare session directories;
|
file |
diff |
annotate
|
| 2019-09-07 |
wenzelm |
avoid overlapping session directories;
|
file |
diff |
annotate
|
| 2019-09-06 |
wenzelm |
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
|
file |
diff |
annotate
|
| 2019-09-03 |
wenzelm |
more dump_checkpoints;
|
file |
diff |
annotate
|
| 2019-08-29 |
wenzelm |
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
|
file |
diff |
annotate
|
| 2019-08-13 |
wenzelm |
NEWS and example for Theory.join_theory;
|
file |
diff |
annotate
|
| 2019-07-23 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| 2019-05-09 |
nipkow |
New version of tries
|
file |
diff |
annotate
|
| 2019-04-16 |
haftmann |
entry point for comprehensive word library
|
file |
diff |
annotate
|
| 2019-04-16 |
haftmann |
tuned theory names
|
file |
diff |
annotate
|
| 2019-04-16 |
haftmann |
integrated Bit_Comparison into Word corpus
|
file |
diff |
annotate
|
| 2019-04-13 |
wenzelm |
clarified group of "main" library sessions;
|
file |
diff |
annotate
|
| 2019-04-09 |
paulson |
new Homology target, depending on HOL-Algebra and HOL-Analysis
|
file |
diff |
annotate
|
| 2019-04-08 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
| 2019-04-07 |
traytel |
bundle for cardinal syntax
|
file |
diff |
annotate
|
| 2019-04-02 |
wenzelm |
more convenient export;
|
file |
diff |
annotate
|
| 2019-03-30 |
haftmann |
experimental commands for proof sketching and exploration
|
file |
diff |
annotate
|
| 2019-03-20 |
wenzelm |
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
|
file |
diff |
annotate
|
| 2018-12-14 |
Manuel Eberl |
Added triangular numbers
|
file |
diff |
annotate
|
| 2019-01-19 |
immler |
automation for unverloading definitions
|
file |
diff |
annotate
|
| 2018-12-30 |
haftmann |
redundant
|
file |
diff |
annotate
|
| 2018-12-28 |
nipkow |
tuned headers etc, added bib-file
|
file |
diff |
annotate
|
| 2018-11-20 |
wenzelm |
tuned -- refining auto-update 15e9ed5b28fb;
|
file |
diff |
annotate
|
| 2018-11-08 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| 2018-11-07 |
haftmann |
dedicated examples for sorting
|
file |
diff |
annotate
|
| 2018-10-17 |
nipkow |
added Array files
|
file |
diff |
annotate
|
| 2018-10-07 |
nipkow |
added Braun_Tree.thy
|
file |
diff |
annotate
|
| 2018-10-01 |
wenzelm |
HOL-SPARK .prv files are no longer written to the file-system;
|
file |
diff |
annotate
|
| 2018-09-30 |
wenzelm |
de-emphasize HOL-SPARK: somewhat outdated;
|
file |
diff |
annotate
|
| 2018-09-05 |
nipkow |
tuned doc
|
file |
diff |
annotate
|
| 2018-07-28 |
wenzelm |
more robust: potentially a workaround for spurious HOL build problems seen by Larry Paulson;
|
file |
diff |
annotate
|
| 2018-07-22 |
eberlm |
Moved Real_Asymp manual
|
file |
diff |
annotate
|