Mercurial
Mercurial
>
repos
>
testboard
/ 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.
repaired incompatibility with new SML version by etaexpansion
19980403, by oheimb
New target HOLUNITY
19980403, by paulson
New UNITY theory
19980403, by paulson
Tidied proofs
19980403, by paulson
Tidied proofs by getting rid of case_tac
19980403, by paulson
improved \tt appearance of many ASCII special symbols like #
19980403, by oheimb
split_all_tac now fails if there is nothing to split
19980402, by oheimb
new theorems
19980402, by paulson
changed if_bool_eq to if_bool_eq_conj
19980402, by paulson
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
19980402, by paulson
New theorems card_Diff_le and card_insert_le; tidied
19980402, by paulson
introduced functions for updating the wrapper lists
19980402, by oheimb
*** empty log message ***
19980402, by oheimb
merge_cs now also merges safe and unsafe wrappers
19980330, by oheimb
generalized appearance of trancl_into_rtrancl and r_into_trancl
19980330, by oheimb
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
less
more

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