Wed, 15 Jan 2025 17:48:38 +0100 merge
nipkow [Wed, 15 Jan 2025 17:48:38 +0100] rev 81812
merge
Wed, 15 Jan 2025 16:45:12 +0100 Compact notation for Suc numerals.
nipkow [Wed, 15 Jan 2025 16:45:12 +0100] rev 81811
Compact notation for Suc numerals.
Wed, 15 Jan 2025 13:55:58 +0100 store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)
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)
Wed, 15 Jan 2025 13:54:28 +0100 make the definition of BNF bounds more easily accessible (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)
Wed, 15 Jan 2025 13:53:25 +0100 avoid theorem name clash (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)
Wed, 15 Jan 2025 13:53:03 +0100 introduce fewer constants in copy_bnf/lift_bnf (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)
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 tip