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.
simplified elimination of chain productions
19950202, by clasohm
binder: optional body pri now [bracketted];
19950127, by wenzelm
improved read_xrules: patterns no longer read twice;
19950127, by wenzelm
*** empty log message ***
19950127, by wenzelm
instance: now automatically includes defs of current thy node as witnesses;
19950127, by wenzelm
binder: optional body pri now [bracketted];
19950127, by wenzelm
added documentation of pwd
19950127, by clasohm
renamed Sign.ambiguity_level to Syntax.ambiguity_level
19950127, by clasohm
moved ambiguity_level from sign.ML to Syntax/syntax.ML
19950127, by clasohm
moved ambiguity_level to Syntax/syntax.ML
19950127, by clasohm
added documentation of Sign.ambiguity_level
19950126, by clasohm
added reference variable ambiguity_level to control ambiguity warnings
19950126, by clasohm
changed due to new .bib files
19950125, by lcp
added optional body priority to binder declaration
19950124, by clasohm
Under RS added cross reference to bind_thm
19950124, by lcp
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
19950124, by lcp
removed mention of FOL_dup_cs
19950124, by lcp
\bibliography now includes crossref.bib
19950124, by lcp
updates for Isabelle942
19950124, by lcp
simplified get_thm a bit
19950123, by clasohm
Replaced ordermap_z_lepoll by ordermap_z_lt, which is
19950120, by lcp
README: Now documents to Tools directory
19950120, by lcp
Deleted semicolon at the end of the qed_goal line, which was preventing
19950120, by lcp
some cosmetic changes
19950119, by nipkow
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
19950119, by clasohm
added optional precedence for body of binder;
19950118, by clasohm
quite a lot of minor and major revisions (inspecting theories, read_axm,
19950118, by wenzelm
empty_def typo
Isabelle942
19950113, by lcp
Proved comp_lam.
19950113, by lcp
Corrected indexing of *datatype
19950113, by lcp
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
less
more

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