Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
Simplified some proofs and made them work for new hyp_subst_tac.
19950413, by lcp
expandshort
19950413, by lcp
Deleted some useless things and made proofs of
19950413, by lcp
Simplified using pattern replacements.
19950413, by lcp
adjusted HOLCF for new hyp_subst_tac
19950413, by regensbu
Defined vv1 using let. Introduced gg1, gg2.
19950413, by lcp
Deleted subset_imp_Un_Diff_eq, as it is identical to
19950413, by lcp
New root file
19950413, by lcp
Redefined OUnion in a definitional manner
19950413, by lcp
Redefined OUnion in a definitional manner, and proved the
19950413, by lcp
Deleted lt_oadd_disj1
19950413, by lcp
Recoded function atomize so that new ways of creating
19950413, by lcp
Proved Int_Diff_eq.
19950413, by lcp
fixed typo
19950413, by lcp
Defined ordinal difference, 
19950413, by lcp
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
19950413, by lcp
Proved lesspoll_succ_iff.
19950413, by lcp
Completely rewrote split_tac. The old one failed in strange circumstances.
19950413, by nipkow
term.ML: add_loose_bnos now returns a list w/o duplicates.
19950412, by nipkow
Added comment to function "loops".
19950411, by nipkow
(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).
19950411, by nipkow
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
19950410, by nipkow
Removed the "exit 1" calls, since now the Makefile does them.
19950410, by nipkow
ROOT.ML: installed new hyp_subst_tac
19950410, by nipkow
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
19950410, by nipkow
Local version of (original) hypsubst: needs no simplifier
19950407, by lcp
Modified proofs for new hyp_subst_tac.
19950406, by lcp
Modified proofs for new hyp_subst_tac, and simplified them.
19950406, by lcp
Received some local definitions from AC_Equiv.thy.
19950406, by lcp
Moved some local definitions to WO6_WO1.ML
19950406, by lcp
Proved if_iff and used it to simplify proof of if_type.
19950406, by lcp
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
19950406, by lcp
Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
19950406, by lcp
Added Id: line
19950406, by lcp
Deleted call to flexflex_tac
19950406, by lcp
Added Id: line
19950406, by lcp
Recoded with help from Toby to use rewriting instead of the
19950406, by lcp
Added comment.
19950406, by lcp
No longer builds the induction structure (from ../Provers/ind.ML)
19950406, by lcp
Loads the local hypsubst.ML. No longer loads ../Provers/ind.ML,
19950406, by lcp
Corrected many errors in the dependencies.
19950406, by lcp
Changed comments and timings.
19950406, by lcp
Updated comments.
19950406, by lcp
Set up for new hyp_subst_tac.
19950406, by lcp
Added Id: line
19950406, by lcp
Fixed typo.
19950406, by lcp
Simplified some proofs and made them work for new hyp_subst_tac.
19950406, by lcp
Now sets loadpath.
19950406, by lcp
Gave tighter priorities to SUM and PROD to reduce ambiguities.
19950406, by lcp
Gave tighter priorities to if, napply and the letforms to
19950406, by lcp
Now sets eta_contract.
19950406, by lcp
Added Id: line
19950406, by lcp
generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)
19950402, by nipkow
replaced 'arities' by 'instance';
19950331, by wenzelm
Simplified using pattern replacements. Added the AC example.
19950331, by lcp
New example of AC Equivalences by Krzysztof Grabczewski
19950331, by lcp
New example of AC Equivalences by Krzysztof Grabczewski
19950331, by lcp
Tried the new addss in many proofs, and tidied others involving simplification.
19950331, by lcp
Tried the new addss in a proof.
19950331, by lcp
Defined addss to perform simplification in a claset.
19950331, by lcp
less
more

(0)
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip