wenzelm [Thu, 12 Jun 2025 12:53:54 +0200] rev 82696
avoid legacy infixes;
wenzelm [Thu, 12 Jun 2025 12:44:47 +0200] rev 82695
discontinue old infixes;
haftmann [Thu, 12 Jun 2025 10:38:02 +0200] rev 82694
eliminated transitional lemma
haftmann [Thu, 12 Jun 2025 10:37:57 +0200] rev 82693
tuned whitespace
haftmann [Thu, 12 Jun 2025 08:03:05 +0200] rev 82692
reorganized more code-only operations
haftmann [Mon, 09 Jun 2025 22:14:38 +0200] rev 82691
more qualified auxiliary operations
paulson <lp15@cam.ac.uk> [Fri, 06 Jun 2025 18:36:29 +0100] rev 82690
Sylvestre's correction to ex_least_nat_le and other tidying
paulson <lp15@cam.ac.uk> [Fri, 06 Jun 2025 16:18:44 +0100] rev 82689
New lemmas for floor/ceiling/round, plus tidying
haftmann [Thu, 05 Jun 2025 15:18:27 +0000] rev 82688
prefer already existing operation to calculate minimum
haftmann [Wed, 04 Jun 2025 19:43:13 +0000] rev 82687
some more lemmas
haftmann [Wed, 04 Jun 2025 19:43:13 +0000] rev 82686
tuned syntax
nipkow [Wed, 04 Jun 2025 09:52:40 +0200] rev 82685
latex error
Manuel Eberl <eberlm@in.tum.de> [Tue, 03 Jun 2025 15:18:54 +0200] rev 82684
HOL: minor additions regarding linear algebra
Manuel Eberl <eberlm@in.tum.de> [Tue, 03 Jun 2025 12:22:58 +0200] rev 82683
HOL-Combinatorics: more lemmas about permutations
wenzelm [Sun, 01 Jun 2025 20:01:22 +0200] rev 82682
merged
wenzelm [Sun, 01 Jun 2025 17:09:23 +0200] rev 82681
tuned;
wenzelm [Sun, 01 Jun 2025 17:06:33 +0200] rev 82680
obsolete (see 22d65e375c01);
wenzelm [Sun, 01 Jun 2025 16:43:09 +0200] rev 82679
more generic parsing of command spans;
support for Thy_Info.get_theories_elements;
wenzelm [Sun, 01 Jun 2025 15:35:28 +0200] rev 82678
tuned;
wenzelm [Sun, 01 Jun 2025 15:30:35 +0200] rev 82677
support for Thy_Info.get_theories_segments, depending on system option "record_theories";
wenzelm [Sun, 01 Jun 2025 13:12:43 +0200] rev 82676
tuned;
haftmann [Sun, 01 Jun 2025 10:29:45 +0200] rev 82675
another default code_unfold rule
haftmann [Sat, 31 May 2025 21:51:08 +0200] rev 82674
generic executable ranges
wenzelm [Sat, 31 May 2025 11:29:10 +0200] rev 82673
clarified signature;
haftmann [Fri, 30 May 2025 08:02:55 +0200] rev 82672
explicit abort for big lattice operations over non-empty sets
haftmann [Fri, 30 May 2025 08:02:54 +0200] rev 82671
prefer explicit operation to make generated code more abstract
haftmann [Fri, 30 May 2025 07:48:17 +0200] rev 82670
tuned theory structure
haftmann [Fri, 30 May 2025 07:47:03 +0200] rev 82669
qualify can_select auxiliary operations
haftmann [Thu, 29 May 2025 14:18:27 +0200] rev 82668
tuned
haftmann [Thu, 29 May 2025 14:17:09 +0200] rev 82667
added lemma