isabelle: Graph

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

adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
adapted fragile proof
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
merged
2010-11-30, by haftmann
more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-30, by haftmann
adapted proofs to slightly changed definitions of congruent(2)
2010-11-30, by haftmann
reorienting iff in Quotient_rel prevents simplifier looping;
2010-11-29, by haftmann
replaced slightly odd locale congruent2 by plain definition
2010-11-29, by haftmann
replaced slightly odd locale congruent by plain definition
2010-11-29, by haftmann
equivI has replaced equiv.intro
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
moved generic definitions about relations from Quotient.thy to Predicate;
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
simplify proof of LIMSEQ_unique
2010-11-30, by huffman
use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-11-30, by huffman
merged
2010-11-30, by huffman
instance list :: (discrete_cpo) discrete_cpo;
2010-11-29, by huffman
merged
2010-11-30, by boehmes
also support higher-order rules for Z3 proof reconstruction
2010-11-29, by boehmes
merged
2010-11-29, by wenzelm
less ghc-specific pragma
2010-11-29, by haftmann
tuned
2010-11-29, by haftmann
updated generated files;
2010-11-29, by wenzelm
added document antiquotation @{file};
2010-11-29, by wenzelm
Parse.liberal_name for document antiquotations and attributes;
2010-11-28, by wenzelm
ML results: enter before printing (cf. Poly/ML SVN 1218);
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by huffman
merged
2010-11-28, by huffman
change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec
2010-11-28, by huffman
add lemma cont2cont_if_bottom
2010-11-27, by huffman
added Parse.literal_fact with proper inner_syntax markup (source position);
2010-11-28, by wenzelm
tuned signature;
2010-11-28, by wenzelm
less frequent sidekick parsing, which is relatively slow;
2010-11-28, by wenzelm
basic setup for bundled Java runtime;
2010-11-28, by wenzelm
updated reference platforms;
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by nipkow
gave more standard finite set rules simp and intro attribute
2010-11-28, by nipkow
more permissive Isabelle_System.mkdir;
2010-11-28, by wenzelm
added 'syntax_declaration' command;
2010-11-28, by wenzelm
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
2010-11-28, by wenzelm
superficial tuning;
2010-11-28, by wenzelm
updated versions;
2010-11-28, by wenzelm
recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-28, by wenzelm
follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);
2010-11-28, by wenzelm
removed HOLCF for now as explicit component
2010-11-28, by krauss
fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-27, by huffman
update web description of HOLCF;
2010-11-27, by huffman
remove HOLCF from build script, since it no longer works
2010-11-27, by huffman
moved directory src/HOLCF to src/HOL/HOLCF;
2010-11-27, by huffman
merged
2010-11-27, by huffman
rename Pcpodef.thy to Cpodef.thy;
2010-11-27, by huffman
renamed several HOLCF theorems (listed in NEWS)
2010-11-27, by huffman
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
2010-11-27, by huffman
rename rep_contlub lemmas to rep_lub
2010-11-27, by huffman
rename function 'match_UU' to 'match_bottom'
2010-11-27, by huffman
rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27, by huffman
merged
2010-11-27, by haftmann

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle