Joachim Breitner [Wed, 23 Jun 2010 10:45:03 +0000 (10:45 +0000)]
langle/rangle for group span

Joachim Breitner [Wed, 23 Jun 2010 10:38:43 +0000 (10:38 +0000)]
Nicer syntax for the Free Group

Joachim Breitner [Wed, 23 Jun 2010 09:58:26 +0000 (09:58 +0000)]
Fix LaTeX build

Joachim Breitner [Wed, 23 Jun 2010 09:50:53 +0000 (09:50 +0000)]
Prove that F_1 = \Z

Joachim Breitner [Mon, 21 Jun 2010 19:13:28 +0000 (19:13 +0000)]
Show that the Free Group over the empty set is the trivial group

Joachim Breitner [Fri, 18 Jun 2010 14:22:36 +0000 (14:22 +0000)]
Prove hom_span

Joachim Breitner [Thu, 17 Jun 2010 23:05:28 +0000 (23:05 +0000)]
Finish universal property

Joachim Breitner [Thu, 17 Jun 2010 00:06:18 +0000 (00:06 +0000)]
Remove trivial lemmas

Joachim Breitner [Thu, 17 Jun 2010 00:02:35 +0000 (00:02 +0000)]
Skip one step

Joachim Breitner [Thu, 17 Jun 2010 00:00:16 +0000 (00:00 +0000)]
Drop unnecessary condition

Joachim Breitner [Wed, 16 Jun 2010 23:55:04 +0000 (23:55 +0000)]
Put lift_cancels_to in a lemmy of its own

Joachim Breitner [Wed, 16 Jun 2010 23:49:24 +0000 (23:49 +0000)]
lift_is_hom
(Very ugly, I am not satisifed)

Joachim Breitner [Wed, 16 Jun 2010 23:48:34 +0000 (23:48 +0000)]
cancels_to_1_unfold: Alternative view on cancels_to_1

Joachim Breitner [Wed, 16 Jun 2010 23:47:46 +0000 (23:47 +0000)]

Joachim Breitner [Tue, 15 Jun 2010 22:51:26 +0000 (22:51 +0000)]
Beginnings of the universal property

Joachim Breitner [Mon, 14 Jun 2010 21:51:55 +0000 (21:51 +0000)]
Theory Generators.thy

Joachim Breitner [Tue, 1 Jun 2010 21:08:53 +0000 (21:08 +0000)]
Do not import List

Joachim Breitner [Sat, 29 May 2010 20:45:36 +0000 (20:45 +0000)]
Give type annotation for free_group, makes Isabelle (and me) happier

Joachim Breitner [Fri, 28 May 2010 19:02:13 +0000 (19:02 +0000)]
Editorial skimming

Joachim Breitner [Fri, 28 May 2010 18:15:45 +0000 (18:15 +0000)]
Show group homomorphism property

Joachim Breitner [Fri, 28 May 2010 15:44:11 +0000 (15:44 +0000)]
Nicer way of proving that something is a group isomorphism

Joachim Breitner [Fri, 28 May 2010 14:34:06 +0000 (14:34 +0000)]
Finish bijectivity of h

Joachim Breitner [Fri, 28 May 2010 14:10:21 +0000 (14:10 +0000)]
Enable quick_and_dirty-mode to work around Isabelle bug

Joachim Breitner [Fri, 28 May 2010 13:14:11 +0000 (13:14 +0000)]
Try to debug the obtain problem

Joachim Breitner [Fri, 28 May 2010 13:14:08 +0000 (13:14 +0000)]
Results that cancelation commutes with renaming elements

Joachim Breitner [Fri, 28 May 2010 13:13:44 +0000 (13:13 +0000)]
Use rename_gens_canceled in inv_fg_closure1

Joachim Breitner [Fri, 28 May 2010 09:39:30 +0000 (09:39 +0000)]
Implement inv1 with apfst

Joachim Breitner [Thu, 27 May 2010 21:22:56 +0000 (21:22 +0000)]
Started to prof that bijective sets produce isomorphic free groups

Joachim Breitner [Thu, 27 May 2010 15:14:52 +0000 (15:14 +0000)]
Define free_groups over a _set_ of generators

Joachim Breitner [Thu, 27 May 2010 15:14:44 +0000 (15:14 +0000)]
Remove thm statement

Joachim Breitner [Thu, 27 May 2010 15:14:40 +0000 (15:14 +0000)]
Show "occuring_generators (normalize l) ⊆ occuring_generators l"

Joachim Breitner [Thu, 27 May 2010 09:50:33 +0000 (09:50 +0000)]
Leverage unfolding

Joachim Breitner [Thu, 27 May 2010 09:15:47 +0000 (09:15 +0000)]
Rename lconf to confluent_cancels_to_1

Joachim Breitner [Thu, 27 May 2010 09:14:47 +0000 (09:14 +0000)]
Removed Andreas’ editorial remarks

Joachim Breitner [Thu, 27 May 2010 08:51:08 +0000 (08:51 +0000)]
Some more cleanup by Andreas Lochbihler

Joachim Breitner [Tue, 25 May 2010 09:27:46 +0000 (09:27 +0000)]
Some cleanup by Daniel Wasserrab

Joachim Breitner [Sat, 22 May 2010 22:42:37 +0000 (22:42 +0000)]
Reformat free_group constdef

Joachim Breitner [Sat, 22 May 2010 22:39:02 +0000 (22:39 +0000)]
Get rid of free_group_set

Joachim Breitner [Sat, 22 May 2010 22:14:53 +0000 (22:14 +0000)]
Get rid of norm_mult

Joachim Breitner [Sat, 22 May 2010 22:07:27 +0000 (22:07 +0000)]
Converted to structured proofs

Joachim Breitner [Sat, 22 May 2010 10:27:09 +0000 (10:27 +0000)]
Initial check-in