Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
3000
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.
adapted proof of finite_converse
19980330, by oheimb
added wf_converse_trancl, adapted proof of wfrec
19980330, by oheimb
added caveat
19980330, by oheimb
added introduction and elimination rules for Univalent
19980330, by oheimb
added Univalent_rel_pow
19980330, by oheimb
removed superfluous use_thy
19980330, by oheimb
removed superfluous translations
19980330, by oheimb
added try, single, many;
19980324, by wenzelm
added cproj', and therefore extended prj
19980324, by oheimb
added cproj', and therefore extended prj
19980324, by oheimb
improved checks
19980324, by oheimb
added o2s
19980324, by oheimb
added finite_acyclic_wf_converse: corrected 8bit chars
19980324, by oheimb
added acyclicI
19980324, by oheimb
added finite_acyclic_wf_converse
19980324, by oheimb
more thms
19980323, by paulson
inverse > converse
19980316, by paulson
inverse > converse
19980316, by paulson
reordered proofs
19980316, by paulson
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
19980313, by wenzelm
renamed not1_or to disj_not1, not2_or to disj_not2
19980312, by oheimb
improved coding of delWrapper and delSWrapper
19980312, by oheimb
addloop: added warning in case of overwriting a looper
19980312, by oheimb
Made mutual simplification of prems a special case.
19980312, by nipkow
Used merge_alists for loopers.
19980312, by nipkow
New, stronger rewrites
19980312, by paulson
The theorem nat_neqE, and some tidying
19980312, by paulson
New laws, mostly generalizing old "pred" ones
19980312, by paulson
spy_analz_tac now handles individual conjuncts properly
19980311, by paulson
new theorem
19980311, by paulson
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
19980311, by paulson
Arith.thy > thy; proved a few new theorems
19980311, by paulson
New Asm_full_simp_tac shortens proof.
19980311, by nipkow
Simplifier
19980311, by nipkow
More Lex.
19980311, by nipkow
New Asm_full_simp_tac led to a loop.
19980311, by nipkow
Mod because of new simplifier.
19980310, by nipkow
Mod because of not1_or.
19980310, by nipkow
Updated proofs because of new simplifier.
19980310, by nipkow
Updated proofs because of new simplification tactics.
19980310, by nipkow
Adapted proofs because of new simplification tactics.
19980310, by nipkow
The new asm_lr_simp_tac is the old asm_full_simp_tac.
19980310, by nipkow
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
19980310, by oheimb
added not1_or and if_eq_cancel to simpset()
19980310, by oheimb
added not1_or and if_eq_cancel to simpset()
19980310, by oheimb
new rewrite rules not1_or, not2_or, and if_eq_cancel
19980310, by oheimb
renamed smart_tac to force_tac, slight improvement of force_tac
19980310, by oheimb
Asm_full_simp_tac now reorients asm c = t to t = c.
19980310, by nipkow
adhoc fix of is_blank;
19980310, by wenzelm
New scanner in abstract form.
19980310, by nipkow
New simplifier flag for mutual simplification.
19980310, by nipkow
Removed expand_split from simpset.
19980310, by nipkow
removed pred;
19980309, by wenzelm
eliminated pred function;
19980309, by wenzelm
Symbol.explode;
19980309, by wenzelm
replaced $LOGNAME by $USER;
19980309, by wenzelm
tuned;
19980309, by wenzelm
Symbol.is_*;
19980309, by wenzelm
adapted to new scanner, baroque chars;
19980309, by wenzelm
Symbol.input;
19980309, by wenzelm
less
more

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