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
wenzelm [Sun, 12 Jan 2025 23:07:50 +0100] rev 81802
merged
wenzelm [Sun, 12 Jan 2025 22:40:56 +0100] rev 81801
tuned messages: more verbosity;
wenzelm [Sun, 12 Jan 2025 22:16:17 +0100] rev 81800
more explicit default_port;
wenzelm [Sun, 12 Jan 2025 22:05:22 +0100] rev 81799
tuned messages;