Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+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.
reimplement proof automation for coinduct rules
20101016, by huffman
add functions mk_imp, mk_all
20101016, by huffman
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
20101015, by huffman
simplify automation of induct proof
20101015, by huffman
add function mk_adm
20101015, by huffman
rewrite proof automation for finite_ind; get rid of case_UU_tac
20101015, by huffman
put constructor argument specs in constr_info type
20101014, by huffman
avoid using Global_Theory.get_thm
20101014, by huffman
include iso_info as part of constr_info type
20101014, by huffman
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
20101014, by huffman
add take_strict_thms field to take_info type
20101014, by huffman
add record type synonym 'constr_info'
20101014, by huffman
add function take_theorems
20101014, by huffman
add type annotation to avoid warning
20101014, by huffman
cleaned up Fun_Cpo.thy; deprecated a few theorem names
20101013, by huffman
edit comments
20101013, by huffman
remove unneeded lemmas Lift_exhaust, Lift_cases
20101012, by huffman
move lemmas from Lift.thy to Cfun.thy
20101012, by huffman
cleaned up Adm.thy
20101012, by huffman
remove unneeded lemmas from Fun_Cpo.thy
20101012, by huffman
remove unused lemmas
20101012, by huffman
reformulate lemma cont2cont_lub and move to Cont.thy
20101012, by huffman
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
20101012, by huffman
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
20101011, by huffman
rename Ffun.thy to Fun_Cpo.thy
20101011, by huffman
remove unused constant 'directed'
20101011, by huffman
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
20101011, by huffman
merged
20101015, by paulson
prevention of selfreferential type environments
20101015, by paulson
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
20101015, by Cezary Kaliszyk
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip