18 months ago ago wenzelm protocol message for export of theory resources;
18 months ago ago wenzelm hexadecimal representation of byte string;
18 months ago ago wenzelm cleanup session output before starting build job;
18 months ago ago nipkow reinstated old lemma name
18 months ago ago nipkow updated to lemma name change
18 months ago ago paulson more tidying
18 months ago ago paulson starting to tidy up Interval_Integral.thy
18 months ago ago nipkow removed asm "finite"
18 months ago ago wenzelm merged
18 months ago ago wenzelm no censorship of view title;
18 months ago ago wenzelm set view title dynamically;
18 months ago ago nipkow tuned
18 months ago ago nipkow tuned
18 months ago ago paulson Some tidying up (mostly regarding summations from 0)
18 months ago ago paulson tidied up Infinite_Products
18 months ago ago immler merged
18 months ago ago paulson a lemma about infinite products
18 months ago ago immler fixed HOL-Analysis
18 months ago ago immler merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
18 months ago ago immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
18 months ago ago paulson merged
18 months ago ago wenzelm tuned -- slightly smaller future closure size;
18 months ago ago wenzelm clarified menu actions;
18 months ago ago wenzelm purge history more thoroughly (see also 3156faac30a7);
18 months ago ago paulson tidying up and using real induction methods
18 months ago ago paulson merged
18 months ago ago paulson merged
18 months ago ago wenzelm clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
18 months ago ago paulson type class generalisations; some work on infinite products
18 months ago ago paulson simplified some messy proofs
18 months ago ago wenzelm avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
18 months ago ago paulson merged
18 months ago ago boehmes prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas
18 months ago ago paulson more general tidying up
18 months ago ago paulson cleaned up more messy proofs
18 months ago ago paulson more defer/prefer
18 months ago ago paulson getting rid of more "defer", etc.
18 months ago ago paulson getting rid of "defer"
18 months ago ago paulson another big cleanup
18 months ago ago paulson merged
18 months ago ago paulson minor typeclass generalisations and junk removal
18 months ago ago paulson merged
18 months ago ago nipkow merged
18 months ago ago paulson more messy proofs
18 months ago ago nipkow new simp modifier: reorient
18 months ago ago paulson small typeclass generalisations
18 months ago ago paulson merged
18 months ago ago wenzelm spelling;
18 months ago ago paulson some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
18 months ago ago paulson more messy proofs redone, and new material
18 months ago ago paulson merged
18 months ago ago wenzelm merged
18 months ago ago wenzelm tuned -- avoid spurious exception trace for "the";
18 months ago ago paulson merged
18 months ago ago haftmann proof of concept for residue rings over int using type numerals
18 months ago ago haftmann more correct error message
18 months ago ago haftmann uniform tagging for printable and non-printable literals
18 months ago ago paulson new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
18 months ago ago paulson merged
18 months ago ago wenzelm more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;