| Thu, 24 Jul 2025 16:44:52 +0200 |
haftmann |
moved / rearranged lemma
|
file |
diff |
annotate
|
| Sun, 01 Jun 2025 10:29:45 +0200 |
haftmann |
another default code_unfold rule
|
file |
diff |
annotate
|
| Fri, 30 May 2025 07:47:03 +0200 |
haftmann |
qualify can_select auxiliary operations
|
file |
diff |
annotate
|
| Thu, 29 May 2025 14:17:08 +0200 |
haftmann |
annotate auxiliary operations explicitly
|
file |
diff |
annotate
|
| Wed, 28 May 2025 17:49:22 +0200 |
haftmann |
more modern qualification of auxiliary operations
|
file |
diff |
annotate
|
| Sun, 18 May 2025 14:33:01 +0000 |
haftmann |
dropped unused ML bindings
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 14:59:57 +0100 |
wenzelm |
more syntax bundles, e.g. to explore terms without notation;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2024 16:05:42 +0000 |
paulson |
Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 19:00:19 +0200 |
wenzelm |
more type information;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2024 15:17:37 +0200 |
wenzelm |
eliminate clones: just one Collect_binder_tr';
|
file |
diff |
annotate
|