Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
120
+120
+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.
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
Limit_csucc: moved to InfDatatype and proved explicitly in
19941216, by lcp
put quotation marks around constant "and" because it is a
19941216, by lcp
added thy_syntax.ML
19941216, by lcp
Defines ZF theory sections (inductive, datatype) at the start/
19941216, by lcp
now also depends upon Finite.thy
19941216, by lcp
converse_converse, converse_prod: renamed from
19941216, by lcp
moved congruence rule conj_cong2 to FOL/IFOL.ML
19941216, by lcp
conj_cong2: new congruence rule
19941216, by lcp
case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted
19941215, by lcp
updated comment;
19941215, by lcp
qconverse_qconverse, qconverse_prod: renamed from
19941215, by lcp
well_ord_iso_predE replaces not_well_ord_iso_pred
19941214, by lcp
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
19941214, by lcp
converse_UN, Diff_eq_0_iff: new
19941214, by lcp
added constants mono_map, ord_iso_map
19941214, by lcp
cardinal_UN_Ord_lt_csucc: added comment
19941214, by lcp
conj_commute,disj_commute: new
19941214, by lcp
changed get_thm to search all parent theories if the theorem is not found
19941214, by clasohm
added bind_thm for theorems defined by "standard ..."
19941214, by clasohm
added any, sprop to pure_types;
19941214, by wenzelm
removed "logic1";
19941214, by wenzelm
removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
19941213, by clasohm
added print_theory that prints stored thms;
19941212, by wenzelm
minor internal changes;
19941209, by wenzelm
improved axioms_of: returns thms as the manual says;
19941209, by wenzelm
removed ZF_Lemmas and added qed_goal
19941209, by clasohm
added warning for already stored theorem to store_thm
19941209, by clasohm
sum_ss: moved down and added the rewrite rules for "case"
19941208, by lcp
leI: added comment
19941208, by lcp
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
19941208, by lcp
sum_ss: deleted because it conflicts with the one in Sum.ML
19941208, by lcp
not_well_ord_iso_pred: removed needless quantifier
19941208, by lcp
UN_upper_cardinal: updated to refer to Card_le_imp_lepoll
19941208, by lcp
sum_lepoll_self, cadd_le_self, prod_lepoll_self,
19941208, by lcp
le_imp_lepoll: renamed to Card_le_imp_lepoll
19941208, by lcp
Card_cardinal_le: new
19941208, by lcp
changed Pure's grammar and the way types are converted to nonterminals
19941208, by clasohm
replaced type_syn by pure_syn in Pure signature
19941208, by clasohm
test_assume_tac: now tries eq_assume_tac on exceptional cases
19941208, by lcp
res_inst_tac: added comments
19941208, by lcp
added qed and qed_goal[w]
19941207, by clasohm
moved first call of store_theory from thy_read.ML to created .thy.ML file
19941207, by clasohm
added bind_thm
19941206, by clasohm
added qed and qed_goal[w]
19941130, by clasohm
added qed_goal for meta_iffD
19941130, by clasohm
replaced "val ... = result()" by "qed ..."
19941130, by clasohm
le_UN_Ord_lt_csucc: added comment
19941129, by lcp
replaced "rules" by "defs"
19941129, by lcp

19941128, by regensbu
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
19941125, by lcp
checks that the recursive sets are Consts before taking
19941125, by lcp
equiv_comp_eq: simplified proof
19941125, by lcp
moved Cantors theorem here from ZF/ex/misc
19941125, by lcp
deepen_tac: modified due to outcome of experiments. Its
19941125, by lcp
added qed_goal[w]
19941125, by clasohm
added blank line
19941125, by lcp
tidied proofs, using fast_tac etc. as much as possible
19941125, by lcp
prove_fun: new; no longer depends upon the version in simpdata.ML
19941125, by lcp
data_domain,Codata_domain: removed replicate; now return one
19941124, by lcp
tidied proofs, using fast_tac etc. as much as possible
19941124, by lcp
added comments on alternative uses of type_intrs/elims
19941124, by lcp
modified for new treatment of mutual recursion
19941124, by lcp
the_equality: more careful use of addSIs and addIs
19941124, by lcp
cons_fun_eq: modified strange uses of classical reasoner
19941124, by lcp
moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
19941124, by lcp
moved version of Cantors theorem to ZF/Perm.ML
19941124, by lcp
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
19941124, by lcp
ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
19941124, by lcp
updated for new deepen_tac
19941124, by lcp
trivial changes
19941124, by lcp
less
more

(0)
120
+120
+1000
+3000
+10000
+30000
tip