Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fri, 15 Oct 1993 10:25:23 +0100 ZF/ex/tf/tree,forest_unfold: streamlined the proofs
changeset
lcp [Fri, 15 Oct 1993 10:25:23 +0100] rev 56
ZF/ex/tf/tree,forest_unfold: streamlined the proofs Updated other inductive def examples as per changes in the package.
Fri, 15 Oct 1993 10:21:01 +0100 ZF/ind-syntax/refl_thin: new
changeset
lcp [Fri, 15 Oct 1993 10:21:01 +0100] rev 55
ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE
(0) -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle