Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
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.
transfer: avoid camel case
20100308, by haftmann
merged
20100307, by huffman
generate separate qualified theorem name for each type's reach and take_lemma
20100307, by huffman
add simp rule LAM_strict
20100307, by huffman
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
20100307, by huffman
merged
20100307, by haftmann
dropped dead code; adhere more closely to standard coding conventions
20100307, by haftmann
merged
20100307, by huffman
arith tactic uses 'priority' instead of 'warning' to print messages
20100307, by huffman
add simp rules about Ints, Nats
20100307, by huffman
add more simp rules for Ints
20100307, by huffman
add lemmas Nats_cases and Nats_induct
20100307, by huffman
generalize some lemmas, and remove a few unnecessary ones
20100307, by huffman
generalize some lemmas from class linordered_ring_strict to linordered_ring
20100306, by huffman
add case_names attribute to casedist and ind rules
20100306, by huffman
add some lemmas about complete lattices
20100306, by huffman
Digesting strings according to SHA1.
20100307, by wenzelm
proper int wrapping for Word32;
20100307, by wenzelm
separate structure Typedecl;
20100307, by wenzelm
modernized structure Object_Logic;
20100307, by wenzelm
modernized structure Local_Defs;
20100307, by wenzelm
merged
20100306, by paulson
merged
20100306, by paulson
simplified
20100306, by paulson
merged
20100306, by haftmann
lemma restrict_complement_singleton_eq
20100306, by haftmann
some lemma refinements
20100306, by haftmann
added Table.thy
20100306, by haftmann
provide ProofContext.def_type depending on "pattern" mode;
20100306, by wenzelm
record_type_tr': more robust strip_fields (printed types are not necessarily wellformed, e.g. in Syntax.pretty_arity);
20100306, by wenzelm
record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
20100306, by wenzelm
eliminated Args.bang_facts (legacy feature);
20100306, by wenzelm
eliminated oldstyle prems;
20100306, by wenzelm
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
20100306, by wenzelm
Some notes on platform support of Isabelle.
20100306, by wenzelm
"private" map_of_map lemma
20100306, by haftmann
added insort_insert
20100306, by haftmann
added dom_option_map, map_of_map_keys
20100306, by haftmann
added bulkload; tuned document
20100306, by haftmann
merged
20100306, by haftmann
merged
20100305, by haftmann
moved lemma map_sorted_distinct_set_unique
20100305, by haftmann
various refinements
20100305, by haftmann
print message when finiteness of domain definition is detected
20100305, by huffman
merged
20100305, by huffman
skip coinduction proofs for indirectrecursive domain definitions
20100305, by huffman
merged
20100306, by wenzelm
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
20100305, by huffman
add comment
20100305, by huffman
move take_proofsrelated stuff to a new section
20100305, by huffman
remove dead code
20100305, by huffman
tuned dead code;
20100305, by wenzelm
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
20100305, by wenzelm
merged
20100305, by wenzelm
fix proof script so 'domain foo = Foo foo' works
20100305, by huffman
fix proof script so qdomain_isomorphism foo = foo' works
20100305, by huffman
finish browser_info: invoke isabelle browser b to ensure that the jar really exists;
20100305, by wenzelm
isabelle browser b: Admin/build only;
20100305, by wenzelm
merged
20100305, by huffman
skip proof of induction rule for indirectrecursive domain definitions
20100305, by huffman
generalized inj_uminus; added strict_mono_imp_inj_on
20100305, by hoelzl
merged
20100305, by hoelzl
Add Lebesgue integral and probability space.
20100304, by hoelzl
Supremum and Infimum on real intervals
20100304, by hoelzl
Rewrite rules for images of minus of intervals
20100304, by hoelzl
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
20100304, by hoelzl
Added natfloor and floor rules for multiplication and power.
20100304, by hoelzl
Generalized setsum_cases
20100304, by hoelzl
Added vimage_inter_cong
20100304, by hoelzl
merged
20100304, by huffman
move coinductionrelated stuff into function prove_coindunction
20100304, by huffman
add function add_qualified_simp_thm
20100304, by huffman
generate lemma take_below, declare chain_take [simp]
20100303, by huffman
switch to polymlsvn;
20100304, by wenzelm
basic simplification of external_prover signature;
20100304, by wenzelm
tuned;
20100304, by wenzelm
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
20100304, by wenzelm
point to http://hginit.com/
20100304, by wenzelm
Simplified a couple of proofs and corrected a comment
20100304, by paulson
lemmas set_map_of_compr, map_of_inject_set
20100304, by haftmann
merged
20100303, by huffman
merged
20100303, by huffman
remove dead code
20100303, by huffman
add infix declarations
20100303, by huffman
remove unnecessary theorem references
20100303, by huffman
remove copy_of_dtyp from domain_axioms.ML
20100303, by huffman
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
20100303, by huffman
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
20100303, by huffman
add function axiomatize_lub_take
20100303, by huffman
move function mk_lub into holcf_library.ML
20100303, by huffman
added extern_syntax;
20100303, by wenzelm
merged
20100303, by haftmann
more uniform naming conventions
20100303, by haftmann
tuned whitespace
20100303, by haftmann
restructured RBT theory
20100303, by haftmann
stats for atpolytest;
20100303, by wenzelm
proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);
20100303, by wenzelm
merged, resolving some basic conflicts;
20100303, by wenzelm
merged
20100303, by krauss
updated patch for hgweb style: now applies to Mercurial 1.4.3 templates
20100303, by krauss
fix fragile proof using old induction rule (cf. bdf8ad377877)
20100303, by krauss
merged
20100303, by hoelzl
replaced \<bullet> with inner
20100302, by himmelma
tuned
20100302, by himmelma
the ordering on real^1 is linear
20100302, by himmelma
merged
20100303, by bulwahn
made smlnj happy
20100302, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
20100302, by bulwahn
adding HOLMutabelle to tests
20100302, by bulwahn
merged
20100303, by haftmann
more explicit naming scheme
20100303, by haftmann
merged
20100302, by huffman
adapt to changed variable name in casedist theorem
20100302, by huffman
remove dependency on domain_syntax.ML
20100302, by huffman
update HOLCF makefile
20100302, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
20100302, by huffman
proof scripts use variable name y for casedist
20100302, by huffman
fixrec and repdef modules import holcf_library
20100302, by huffman
use y as variable name in casedist, like datatype package
20100302, by huffman
proper names for types cfun, sprod, ssum
20100302, by huffman
less
more

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