Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
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.
removing something that probably slipped into the Quotient_List theory
20101019, by bulwahn
Quotient package: partial equivalence introduction
20101019, by Cezary Kaliszyk
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
20101018, by Christian Urban
remove dead code
20101016, by huffman
remove old uses of 'simp_tac HOLCF_ss'
20101016, by huffman
merged
20101016, by huffman
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
20101016, by huffman
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
FSet tuned
20101015, by Cezary Kaliszyk
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
20101015, by Cezary Kaliszyk
NEWS
20101014, by krauss
removed output syntax "'a ~=> 'b" for "'a => 'b option"
20101010, by krauss
reactivated
20101013, by krauss
slightly more robust proof
20101012, by krauss
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
20101011, by huffman
merged
20101011, by huffman
move all bifinite class instances to Bifinite.thy
20101009, by huffman
rename class 'sfp' to 'bifinite'
20101008, by huffman
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
20101007, by huffman
add lemma typedef_ideal_completion
20101007, by huffman
remove unused lemmas
20101007, by huffman
remove Infinite_Set from ROOT.ML
20101007, by huffman
remove some junk that made it in by accient
20101007, by huffman
"setup" in theory
20101011, by blanchet
added "trace_meson" configuration option, replacing oldfashioned reference
20101011, by blanchet
added "trace_metis" configuration option, replacing oldfashioned references
20101011, by blanchet
do not mention unqualified names, now that 'global' and 'local' are gone
20101010, by krauss
simplified proof
20101010, by nipkow
avoid generating several formulas with the same name ("tfrees")
20101010, by blanchet
major reorganization/simplification of HOLCF type classes:
20101006, by huffman
add lemma finite_deflation_intro
20101005, by Brian Huffman
less
more

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