| Thu, 24 May 2012 17:25:53 +0200 | wenzelm | tuned proofs; | changeset | files |
| Thu, 24 May 2012 17:05:30 +0200 | wenzelm | reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy"); | changeset | files |
| Thu, 24 May 2012 15:54:38 +0200 | wenzelm | merged | changeset | files |
| Thu, 24 May 2012 15:11:53 +0200 | blanchet | update Satallax setup based on evaluation | changeset | files |
| Thu, 24 May 2012 15:03:06 +0200 | kuncar | merged | changeset | files |
| Thu, 24 May 2012 14:20:25 +0200 | kuncar | drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems | changeset | files |
| Thu, 24 May 2012 14:20:23 +0200 | kuncar | prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule | changeset | files |
| Thu, 24 May 2012 15:01:29 +0200 | blanchet | gracefully handle definition-looking premises | changeset | files |