2 months ago haftmann 2019-06-14 avoid pseudo-collection to be used in generated proofs
2 months ago haftmann 2019-06-14 moved comment to approproiate place
2 months ago haftmann 2019-06-14 removed outcommented example which seems not to work as advertized
2 months ago haftmann 2019-06-14 clear separation of types for bits (False / True) and Z2 (0 / 1)
2 months ago haftmann 2019-06-14 generalized type classes for parity to cover word types also, which contain zero divisors
2 months ago haftmann 2019-06-14 slightly more specialized name for type class
2 months ago haftmann 2019-06-14 dropped weaker legacy alias
2 months ago haftmann 2019-06-14 slightly more stringent ordering of theorems
2 months ago haftmann 2019-06-14 removed relics of ASCII syntax for indexed big operators
2 months ago haftmann 2019-06-14 dropped former legacy input abbreviations
2 months ago haftmann 2019-06-14 using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
2 months ago haftmann 2019-06-14 prefer fixed simpset for proof procedure
2 months ago haftmann 2019-06-14 tuned file system structure
2 months ago haftmann 2019-06-14 avoid spammed sledgehammer proofs
2 months ago nipkow 2019-06-11 added lemmas
2 months ago wenzelm 2019-06-09 proper URL;
2 months ago wenzelm 2019-06-09 merged;
2 months ago wenzelm 2019-06-09 Added tag Isabelle2019 for changeset 83774d669b51
2 months ago blanchet 2019-06-07 handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
2 months ago wenzelm 2019-06-04 tuned;
2 months ago wenzelm 2019-06-04 tuned;
2 months ago wenzelm 2019-06-04 backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
2 months ago wenzelm 2019-06-04 unused;
2 months ago wenzelm 2019-06-04 tuned messages;
2 months ago wenzelm 2019-06-04 proper context;
2 months ago wenzelm 2019-06-04 misc tuning and clarification, notably wrt. flow of context;
2 months ago wenzelm 2019-06-04 proper context;
2 months ago wenzelm 2019-06-04 proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
2 months ago wenzelm 2019-06-04 unused;
2 months ago wenzelm 2019-06-04 misc tuning and clarification, notably wrt. flow of context;
2 months ago wenzelm 2019-06-04 proper context;
2 months ago wenzelm 2019-06-04 proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
2 months ago wenzelm 2019-06-03 more structural integrity;
2 months ago wenzelm 2019-06-03 tuned;
2 months ago wenzelm 2019-06-03 more structural integrity;
2 months ago wenzelm 2019-06-03 clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
2 months ago wenzelm 2019-06-03 tuned;
2 months ago wenzelm 2019-06-03 clarified signature;
2 months ago wenzelm 2019-06-03 tuned whitespace;
2 months ago wenzelm 2019-06-03 clarified context: prefer abstract Variable.auto_fixes;
2 months ago wenzelm 2019-06-03 tuned;
2 months ago wenzelm 2019-06-03 tuned signature;
2 months ago wenzelm 2019-06-03 redundant: default is false;
2 months ago wenzelm 2019-06-01 tuned imports -- accommodate scala-2.13.0-RC3;
2 months ago wenzelm 2019-06-01 tuned -- accommodate scala-2.13.0-RC3;
2 months ago wenzelm 2019-06-01 merged
2 months ago wenzelm 2019-06-01 Added tag Isabelle2019-RC4 for changeset ad2d84c42380 Isabelle2019
2 months ago wenzelm 2019-06-01 hint on printing via Web browser;
2 months ago wenzelm 2019-05-28 tuned;
2 months ago nipkow 2019-05-31 tuned proof
2 months ago nipkow 2019-05-31 tuned
2 months ago wenzelm 2019-05-27 merged
2 months ago wenzelm 2019-05-27 more direct invocation of Windows exe: avoid extra bash, cygpath, exec;
2 months ago wenzelm 2019-05-27 tuned whitespace;
2 months ago wenzelm 2019-05-27 updated to bash_process-1.2.3: rebuild on current reference PLATFORMS;
2 months ago wenzelm 2019-05-25 Added tag Isabelle2019-RC3 for changeset 85de4fdec61b
2 months ago wenzelm 2019-05-24 more robust InstallPath (amending 4ce07be8ba17): self-directory may be odd temp dir produced by browser "Run" operation;
3 months ago wenzelm 2019-05-24 avoid extra subprocess -- potentially more robust on Cygwin;
3 months ago wenzelm 2019-05-24 updated to cygwin-20190524;
3 months ago wenzelm 2019-05-21 proper version;