| Fri, 13 Jun 2025 20:59:51 +0200 |
nipkow |
the canonical homomorphism should be [simp]
default tip
|
changeset |
files
|
| Fri, 13 Jun 2025 17:16:53 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 13 Jun 2025 17:16:38 +0200 |
nipkow |
added minus functions on lists
|
changeset |
files
|
| Fri, 13 Jun 2025 15:18:16 +0200 |
wenzelm |
more robust GUI setup via Java, instead of shell script;
|
changeset |
files
|
| Thu, 12 Jun 2025 16:54:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 12 Jun 2025 12:59:17 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Thu, 12 Jun 2025 12:53:54 +0200 |
wenzelm |
avoid legacy infixes;
|
changeset |
files
|
| Thu, 12 Jun 2025 12:44:47 +0200 |
wenzelm |
discontinue old infixes;
|
changeset |
files
|
| Thu, 12 Jun 2025 10:38:02 +0200 |
haftmann |
eliminated transitional lemma
|
changeset |
files
|
| Thu, 12 Jun 2025 10:37:57 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Thu, 12 Jun 2025 08:03:05 +0200 |
haftmann |
reorganized more code-only operations
|
changeset |
files
|
| Mon, 09 Jun 2025 22:14:38 +0200 |
haftmann |
more qualified auxiliary operations
|
changeset |
files
|
| Fri, 06 Jun 2025 18:36:29 +0100 |
paulson |
Sylvestre's correction to ex_least_nat_le and other tidying
|
changeset |
files
|
| Fri, 06 Jun 2025 16:18:44 +0100 |
paulson |
New lemmas for floor/ceiling/round, plus tidying
|
changeset |
files
|
| Thu, 05 Jun 2025 15:18:27 +0000 |
haftmann |
prefer already existing operation to calculate minimum
|
changeset |
files
|
| Wed, 04 Jun 2025 19:43:13 +0000 |
haftmann |
some more lemmas
|
changeset |
files
|
| Wed, 04 Jun 2025 19:43:13 +0000 |
haftmann |
tuned syntax
|
changeset |
files
|
| Wed, 04 Jun 2025 09:52:40 +0200 |
nipkow |
latex error
|
changeset |
files
|
| Tue, 03 Jun 2025 15:18:54 +0200 |
Manuel Eberl |
HOL: minor additions regarding linear algebra
|
changeset |
files
|
| Tue, 03 Jun 2025 12:22:58 +0200 |
Manuel Eberl |
HOL-Combinatorics: more lemmas about permutations
|
changeset |
files
|
| Sun, 01 Jun 2025 20:01:22 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 01 Jun 2025 17:09:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Jun 2025 17:06:33 +0200 |
wenzelm |
obsolete (see 22d65e375c01);
|
changeset |
files
|
| Sun, 01 Jun 2025 16:43:09 +0200 |
wenzelm |
more generic parsing of command spans;
|
changeset |
files
|
| Sun, 01 Jun 2025 15:35:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Jun 2025 15:30:35 +0200 |
wenzelm |
support for Thy_Info.get_theories_segments, depending on system option "record_theories";
|
changeset |
files
|
| Sun, 01 Jun 2025 13:12:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Jun 2025 10:29:45 +0200 |
haftmann |
another default code_unfold rule
|
changeset |
files
|
| Sat, 31 May 2025 21:51:08 +0200 |
haftmann |
generic executable ranges
|
changeset |
files
|
| Sat, 31 May 2025 11:29:10 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 30 May 2025 08:02:55 +0200 |
haftmann |
explicit abort for big lattice operations over non-empty sets
|
changeset |
files
|
| Fri, 30 May 2025 08:02:54 +0200 |
haftmann |
prefer explicit operation to make generated code more abstract
|
changeset |
files
|
| Fri, 30 May 2025 07:48:17 +0200 |
haftmann |
tuned theory structure
|
changeset |
files
|
| Fri, 30 May 2025 07:47:03 +0200 |
haftmann |
qualify can_select auxiliary operations
|
changeset |
files
|
| Thu, 29 May 2025 14:18:27 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 29 May 2025 14:17:09 +0200 |
haftmann |
added lemma
|
changeset |
files
|
| Thu, 29 May 2025 14:17:08 +0200 |
haftmann |
annotate auxiliary operations explicitly
|
changeset |
files
|
| Thu, 29 May 2025 11:15:48 +0200 |
haftmann |
more correct language
|
changeset |
files
|
| Wed, 28 May 2025 17:49:22 +0200 |
haftmann |
more modern qualification of auxiliary operations
|
changeset |
files
|
| Sat, 24 May 2025 09:06:26 +0200 |
haftmann |
move legacy simplifier interfaces into separate file
|
changeset |
files
|
| Thu, 22 May 2025 19:59:43 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Wed, 21 May 2025 20:44:12 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 21 May 2025 22:03:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 May 2025 21:51:56 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 May 2025 21:36:59 +0200 |
wenzelm |
update jedit component;
|
changeset |
files
|
| Wed, 21 May 2025 17:42:38 +0200 |
wenzelm |
clarified colors for "dark" theme -- requires to update jedit component;
|
changeset |
files
|
| Wed, 21 May 2025 16:34:03 +0200 |
wenzelm |
suppress other icon themes: always use default "tango" (which includes "idea-icons") -- requires to update jedit component;
|
changeset |
files
|
| Wed, 21 May 2025 15:13:31 +0200 |
wenzelm |
clarified patches: this is hardly modular anymore;
|
changeset |
files
|
| Wed, 21 May 2025 15:09:48 +0200 |
wenzelm |
redundant;
|
changeset |
files
|
| Wed, 21 May 2025 21:48:42 +0200 |
Manuel Eberl |
three lemmas for HOL-Complex_Analysis, HOL-Computational_Algebra
|
changeset |
files
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
provide list-valued interface for simp rules
|
changeset |
files
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
provide modern interface for solvers
|
changeset |
files
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
provide modern interface for loopers
|
changeset |
files
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
tuned argument order an internal names
|
changeset |
files
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
typo
|
changeset |
files
|
| Wed, 21 May 2025 14:38:46 +0200 |
wenzelm |
proper NEWS + CONTRIBUTORS;
|
changeset |
files
|
| Wed, 21 May 2025 14:33:57 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Wed, 21 May 2025 13:50:40 +0200 |
wenzelm |
more concise Isabelle/ML;
|
changeset |
files
|
| Wed, 21 May 2025 10:30:35 +0200 |
haftmann |
reordered signature
|
changeset |
files
|
| Wed, 21 May 2025 10:30:34 +0200 |
haftmann |
prefer Simplifier over bootstrap-only Raw_Simplifier
|
changeset |
files
|