darcs-mirror-afp-Free-Groups.git
2010-06-23 Joachim Breitnerlangle/rangle for group span master
2010-06-23 Joachim BreitnerNicer syntax for the Free Group
2010-06-23 Joachim BreitnerFix LaTeX build
2010-06-23 Joachim BreitnerProve that F_1 = \Z
2010-06-21 Joachim BreitnerShow that the Free Group over the empty set is the...
2010-06-18 Joachim BreitnerProve hom_span
2010-06-17 Joachim BreitnerFinish universal property
2010-06-17 Joachim BreitnerRemove trivial lemmas
2010-06-17 Joachim BreitnerSkip one step
2010-06-17 Joachim BreitnerDrop unnecessary condition
2010-06-16 Joachim BreitnerPut lift_cancels_to in a lemmy of its own
2010-06-16 Joachim Breitnerlift_is_hom
2010-06-16 Joachim Breitnercancels_to_1_unfold: Alternative view on cancels_to_1
2010-06-16 Joachim Breitnerm_concat and lemmas about
2010-06-15 Joachim BreitnerBeginnings of the universal property
2010-06-14 Joachim BreitnerTheory Generators.thy
2010-06-01 Joachim BreitnerDo not import List
2010-05-29 Joachim BreitnerGive type annotation for free_group, makes Isabelle...
2010-05-28 Joachim BreitnerEditorial skimming
2010-05-28 Joachim BreitnerShow group homomorphism property
2010-05-28 Joachim BreitnerNicer way of proving that something is a group isomorphism
2010-05-28 Joachim BreitnerFinish bijectivity of h
2010-05-28 Joachim BreitnerEnable quick_and_dirty-mode to work around Isabelle bug
2010-05-28 Joachim BreitnerTry to debug the obtain problem
2010-05-28 Joachim BreitnerResults that cancelation commutes with renaming elements
2010-05-28 Joachim BreitnerUse rename_gens_canceled in inv_fg_closure1
2010-05-28 Joachim BreitnerImplement inv1 with apfst
2010-05-27 Joachim BreitnerStarted to prof that bijective sets produce isomorphic...
2010-05-27 Joachim BreitnerDefine free_groups over a _set_ of generators
2010-05-27 Joachim BreitnerRemove thm statement
2010-05-27 Joachim BreitnerShow "occuring_generators (normalize l) ⊆ occuring_gene...
2010-05-27 Joachim BreitnerLeverage unfolding
2010-05-27 Joachim BreitnerRename lconf to confluent_cancels_to_1
2010-05-27 Joachim BreitnerRemoved Andreas’ editorial remarks
2010-05-27 Joachim BreitnerSome more cleanup by Andreas Lochbihler
2010-05-25 Joachim BreitnerSome cleanup by Daniel Wasserrab
2010-05-22 Joachim BreitnerReformat free_group constdef
2010-05-22 Joachim BreitnerGet rid of free_group_set
2010-05-22 Joachim BreitnerGet rid of norm_mult
2010-05-22 Joachim BreitnerConverted to structured proofs
2010-05-22 Joachim BreitnerInitial check-in