Mon, 16 Sep 2013 16:48:08 +0200 | panny | merge | changeset | files |
Mon, 16 Sep 2013 15:03:23 +0200 | panny | prove simp theorems for newly generated definitions | changeset | files |
Mon, 16 Sep 2013 15:30:20 +0200 | kuncar | example using restoring Transfer/Lifting context | changeset | files |
Mon, 16 Sep 2013 15:30:20 +0200 | kuncar | use lifting_forget for deregistering numeric types as a quotient type | changeset | files |
Mon, 16 Sep 2013 15:30:17 +0200 | kuncar | restoring Transfer/Lifting context | changeset | files |
Mon, 16 Sep 2013 11:54:57 +0200 | kuncar | make ML function for deleting quotients public | changeset | files |
Mon, 16 Sep 2013 11:54:57 +0200 | kuncar | public access to the raw transfer rules - for restoring transferring | changeset | files |