isabelle: Changelog

nipkow [Wed, 15 Jan 2025 17:48:38 +0100] rev 81812

merge

nipkow [Wed, 15 Jan 2025 16:45:12 +0100] rev 81811

Compact notation for Suc numerals.

traytel [Wed, 15 Jan 2025 13:55:58 +0100] rev 81810

store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)

traytel [Wed, 15 Jan 2025 13:54:28 +0100] rev 81809

make the definition of BNF bounds more easily accessible (by Jan van Brügge)

traytel [Wed, 15 Jan 2025 13:53:25 +0100] rev 81808

avoid theorem name clash (by Jan van Brügge)

traytel [Wed, 15 Jan 2025 13:53:03 +0100] rev 81807

introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)

paulson <lp15@cam.ac.uk> [Tue, 14 Jan 2025 22:35:03 +0000] rev 81806

Some work on an ancient theory file. And a weird failure in Float.thy

paulson <lp15@cam.ac.uk> [Tue, 14 Jan 2025 21:50:44 +0000] rev 81805

simplified old proofs

paulson <lp15@cam.ac.uk> [Tue, 14 Jan 2025 18:46:58 +0000] rev 81804

polished messy proofs

nipkow [Mon, 13 Jan 2025 21:17:40 +0100] rev 81803

moved lemmas to book

isabelle