Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -15 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Examples/FSet3.thy
2010-01-13 Christian Urban merged file | diff | annotate
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM" file | diff | annotate
2010-01-12 Cezary Kaliszyk Change OO to OOO in FSet3. file | diff | annotate
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM" file | diff | annotate
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples. file | diff | annotate
2010-01-08 Cezary Kaliszyk Experimients with fconcat_insert file | diff | annotate
2010-01-08 Cezary Kaliszyk Proved concat_empty. file | diff | annotate
2010-01-06 Cezary Kaliszyk Tried to prove the lemma manually; only left with quotient proofs. file | diff | annotate
2010-01-06 Cezary Kaliszyk Sledgehammer bug. file | diff | annotate
2009-12-30 cu some small changes file | diff | annotate
2009-12-27 Christian Urban added a functor that allows checking what is added to the theorem lists file | diff | annotate
2009-12-26 Christian Urban corrected wrong [quot_respect] attribute; tuned file | diff | annotate
2009-12-26 Christian Urban added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML) file | diff | annotate
2009-12-26 Christian Urban as expected problems occure when lifting concat lemmas file | diff | annotate
2009-12-24 Christian Urban made the quotient_type definition more like typedef; now type variables need to be explicitly given file | diff | annotate
less more (0) -15 tip
nominal2