Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
prove_fun now includes equalityI. Added the rewrite rules
19950112, by lcp
Proved sum_bij, sum_ord_iso_cong, prod_bij,
19950112, by lcp
Proved case_cong and case_case.
19950112, by lcp
Renamed single_fun to singleton_fun.
19950112, by lcp
Now also depends upon equalities.thy, allowing use of the
19950112, by lcp
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
19950112, by lcp
Removed spurious comment about eq_cs
19950112, by lcp
Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML
19950112, by lcp
Now depends upon Bool, so that 1 and 2 are defined
19950112, by lcp
Moved theorems Ord_cases_lemma and Ord_cases here from Univ,
19950112, by lcp
Added constants Ord_alt, ++, **
19950112, by lcp
Proved equivalence of Ord and Ord_alt. Proved
19950112, by lcp
Proved ord_isoI, ord_iso_refl. Simplified proof of
19950111, by lcp
Proved cadd_cmult_distrib.
19950111, by lcp
Now proof of Ord_jump_cardinal uses
19950111, by lcp
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
19950111, by lcp
pretty_gram: now sorts productions;
19950111, by wenzelm
removed print_sign, print_axioms;
19950111, by wenzelm
slightly changed OFCLASS syntax;
19950111, by wenzelm
fixed minor typos;
19950102, by wenzelm
added;
19950102, by wenzelm
RepFun_eq_0_iff, RepFun_0: new
19941223, by lcp
Moved Transset_includes_summands and Transset_sum_Int_subset
19941223, by lcp
Reindented declarations; declared the number 2
19941223, by lcp
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
19941223, by lcp
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
19941223, by lcp
singleton_iff: new
19941223, by lcp
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
19941223, by lcp
Added Krzysztof's constants lesspoll and Finite
19941223, by lcp
Added Krzysztof's theorem pred_Memrel
19941223, by lcp
Moved Transset_includes_summands and Transset_sum_Int_subset to
19941223, by lcp
natE0: deleted, since unused
19941223, by lcp
Changed succ(1) to 2 in in_VLimit, two_in_univ
19941223, by lcp
csquare_rel_def: renamed k to K
19941223, by lcp
inj_apply_equality: new
19941223, by lcp
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
19941223, by lcp
empty_fun: generalized from > to Pi
19941223, by lcp
Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
19941223, by lcp
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
19941223, by lcp
Added Krzysztof's theorem disj_imp_disj
19941223, by lcp
Id: marker.
19941221, by lcp
Added comments and Id: marker.
19941221, by lcp
Added comments and Id: marker.
19941221, by lcp
Tools description, largely taken from ../README
19941221, by lcp
Moved description of tools to Tools/README
19941221, by lcp
ord_iso_rvimage: new
19941220, by lcp
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
19941220, by lcp
qed is a utility that makes ML files store the defined theories in Isabelle's
19941220, by clasohm
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
19941220, by lcp
Used bind_thm to store domain_rel_subset and range_rel_subset
19941220, by lcp
removed quotes around "Datatype",
19941219, by lcp
removed quotes around "Inductive"
19941219, by lcp
ran expandshort script
19941219, by lcp
ran expandshort script
19941219, by lcp
removed quotes around "Inductive"
19941219, by lcp
added true theory dependencies
19941219, by lcp
ran expandshort script
19941219, by lcp
changed useless "qed" calls for lemmas back to uses of "result",
19941216, by lcp
Defines ZF theory sections (inductive, datatype) at the start/
19941216, by lcp
Added Limit_csucc from CardinalArith
19941216, by lcp
less
more

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