summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality

more robust Swing_Thread.now: allow body to fail;

tuned proofs;

reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");

merged

update Satallax setup based on evaluation

merged

drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

gracefully handle definition-looking premises