deleted obsolete group formalization
authorpaulson
Mon May 05 18:30:48 2003 +0200 (2003-05-05)
changeset 139590e0553e7d696
parent 13958 c1c67582c9b5
child 13960 70f9158b6695
deleted obsolete group formalization
src/HOL/GroupTheory/Group.thy
src/HOL/GroupTheory/README.html
src/HOL/GroupTheory/ROOT.ML
src/HOL/GroupTheory/document/root.tex
     1.1 --- a/src/HOL/GroupTheory/Group.thy	Mon May 05 18:23:40 2003 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,369 +0,0 @@
     1.4 -(*  Title:      HOL/GroupTheory/Group
     1.5 -    ID:         $Id$
     1.6 -    Author:     Florian Kammueller, with new proofs by L C Paulson
     1.7 -*)
     1.8 -
     1.9 -header{*Group Theory Using Locales*}
    1.10 -
    1.11 -theory Group = FuncSet:
    1.12 -
    1.13 -subsection{*Semigroups*}
    1.14 -
    1.15 -record 'a semigroup =
    1.16 -  carrier :: "'a set"    
    1.17 -  sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>\<index>" 65)
    1.18 -
    1.19 -locale semigroup = struct S +
    1.20 -  assumes sum_funcset: "sum S \<in> carrier S \<rightarrow> carrier S \<rightarrow> carrier S"
    1.21 -      and sum_assoc:   
    1.22 -            "[|x \<in> carrier S; y \<in> carrier S; z \<in> carrier S|] 
    1.23 -             ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    1.24 -
    1.25 -constdefs
    1.26 -  order     :: "(('a,'b) semigroup_scheme) => nat"
    1.27 -   "order(S) == card(carrier S)"
    1.28 -
    1.29 -
    1.30 -(*Overloading is impossible because of the way record types are represented*)
    1.31 -constdefs
    1.32 -  subsemigroup  :: "['a set, ('a,'b) semigroup_scheme] => bool"
    1.33 -   "subsemigroup H G == 
    1.34 -	H <= carrier G & 
    1.35 -	semigroup G &
    1.36 -        semigroup (G(|carrier:=H|))"
    1.37 -
    1.38 -(*a characterization of subsemigroups *)
    1.39 -lemma (in semigroup) subsemigroupI:
    1.40 -     "[| H <= carrier S; 
    1.41 -         !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |] 
    1.42 -      ==> subsemigroup H S"
    1.43 -apply (insert prems) 
    1.44 -apply (simp add: semigroup_def subsemigroup_def, clarify) 
    1.45 -apply (blast intro: funcsetI) 
    1.46 -done
    1.47 -
    1.48 -
    1.49 -subsection{*Groups*}
    1.50 -
    1.51 -record 'a group = "'a semigroup" +
    1.52 -  gminus :: "'a \<Rightarrow> 'a"    ("(\<ominus>\<index>_)" [81] 80)
    1.53 -  zero :: 'a    ("\<zero>\<index>")
    1.54 -
    1.55 -locale group = semigroup G +
    1.56 -  assumes minus_funcset: "gminus G \<in> carrier G \<rightarrow> carrier G"
    1.57 -      and zero_closed [iff]: 
    1.58 -            "zero G \<in> carrier G"
    1.59 -      and left_minus [simp]: 
    1.60 -            "x \<in> carrier G ==> (\<ominus>x) \<oplus> x = \<zero>"
    1.61 -      and left_zero [simp]:
    1.62 -            "x \<in> carrier G ==> \<zero> \<oplus> x = x"
    1.63 -
    1.64 -
    1.65 -constdefs
    1.66 -  Group :: "('a,'b) group_scheme set"
    1.67 -   "Group == Collect group"
    1.68 -
    1.69 -lemma [simp]: "(G \<in> Group) = (group G)"
    1.70 -by (simp add: Group_def) 
    1.71 -
    1.72 -lemma "group G ==> semigroup G"
    1.73 -by (simp add: group_def semigroup_def) 
    1.74 -
    1.75 -
    1.76 -locale abelian_group = group +
    1.77 -  assumes sum_commute: "[|x \<in> carrier G; y \<in> carrier G|] ==> x \<oplus> y = y \<oplus> x"
    1.78 -
    1.79 -lemma abelian_group_iff:
    1.80 -     "abelian_group G = 
    1.81 -      (group G & (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. sum G x y = sum G y x))"
    1.82 -by (force simp add: abelian_group_axioms_def abelian_group_def group_def) 
    1.83 -
    1.84 -
    1.85 -subsection{*Basic Group Theory Theorems*}
    1.86 -
    1.87 -lemma (in semigroup) sum_closed [simp]: 
    1.88 -     "[|x \<in> carrier S; y \<in> carrier S|] ==> (x \<oplus> y) \<in> carrier S"
    1.89 -apply (insert sum_funcset) 
    1.90 -apply (blast dest: funcset_mem) 
    1.91 -done
    1.92 -
    1.93 -lemma (in group) minus_closed [simp]: 
    1.94 -     "x \<in> carrier G ==> (\<ominus>x) \<in> carrier G"
    1.95 -apply (insert minus_funcset) 
    1.96 -apply (blast dest: funcset_mem) 
    1.97 -done
    1.98 -
    1.99 -lemma (in group) left_cancellation:
   1.100 -  assumes "x \<oplus> y  =  x \<oplus> z"
   1.101 -          "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
   1.102 -  shows "y = z"
   1.103 -proof -
   1.104 -  have "((\<ominus>x) \<oplus> x) \<oplus> y = ((\<ominus>x) \<oplus> x) \<oplus> z" 
   1.105 -        by (simp only: prems minus_closed sum_assoc) 
   1.106 -  thus ?thesis by (simp add: prems) 
   1.107 -qed
   1.108 -
   1.109 -lemma (in group) left_cancellation_iff [simp]:
   1.110 -     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]  
   1.111 -      ==> (x \<oplus> y  =  x \<oplus> z) = (y = z)"
   1.112 -by (blast intro: left_cancellation)
   1.113 -
   1.114 -
   1.115 -subsection{*The Other Directions of Basic Lemmas*}
   1.116 -
   1.117 -lemma (in group) right_zero [simp]: "x \<in> carrier G ==> x \<oplus> \<zero> = x"
   1.118 -apply (rule left_cancellation [of "(\<ominus>x)"])
   1.119 -apply (auto simp add: sum_assoc [symmetric])
   1.120 -done
   1.121 -
   1.122 -lemma (in group) idempotent_imp_zero: "[| x \<in> carrier G; x \<oplus> x = x |] ==> x=\<zero>"
   1.123 -by (rule left_cancellation [of x], auto)
   1.124 -
   1.125 -lemma (in group) right_minus [simp]: "x \<in> carrier G ==> x \<oplus> (\<ominus>x) = \<zero>"
   1.126 -apply (rule idempotent_imp_zero)
   1.127 -apply (simp_all add: sum_assoc [symmetric])
   1.128 -apply (simp add: sum_assoc)
   1.129 -done
   1.130 -
   1.131 -lemma (in group) minus_unique:
   1.132 -     "[| x \<in> carrier G; y \<in> carrier G; x \<oplus> y = \<zero> |] ==> y = (\<ominus>x)"
   1.133 -apply (rule left_cancellation [of x], auto)
   1.134 -done
   1.135 -
   1.136 -lemma (in group) minus_minus [simp]:
   1.137 -     "x \<in> carrier G ==> \<ominus>(\<ominus>x) = x"
   1.138 -apply (rule left_cancellation [of "(\<ominus>x)"])
   1.139 -apply auto
   1.140 -done
   1.141 -
   1.142 -lemma (in group) minus_sum:
   1.143 -     "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus>(x \<oplus> y) = (\<ominus>y) \<oplus> (\<ominus>x)"
   1.144 -apply (rule minus_unique [symmetric])
   1.145 -apply (simp_all add: sum_assoc [symmetric])
   1.146 -apply (simp add: sum_assoc) 
   1.147 -done
   1.148 -
   1.149 -lemma (in group) right_cancellation:
   1.150 -     "[| y \<oplus> x =  z \<oplus> x;   
   1.151 -         x \<in> carrier G; y \<in> carrier G; z \<in> carrier G|] ==> y = z"
   1.152 -apply (drule arg_cong [of concl: "%z. z \<oplus> (\<ominus>x)"])
   1.153 -apply (simp add: sum_assoc)
   1.154 -done
   1.155 -
   1.156 -lemma (in group) right_cancellation_iff [simp]:
   1.157 -     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]  
   1.158 -      ==> (y \<oplus> x =  z \<oplus> x) = (y = z)"
   1.159 -by (blast intro: right_cancellation)
   1.160 -
   1.161 -
   1.162 -subsection{*The Subgroup Relation*}
   1.163 -
   1.164 -constdefs  
   1.165 -  subgroup  :: "['a set, ('a,'b) group_scheme] => bool"
   1.166 -   "subgroup H G == 
   1.167 -	H <= carrier G & 
   1.168 -	group G &
   1.169 -        group (G(|carrier:=H|))";
   1.170 -
   1.171 -
   1.172 -text{*Since @{term H} is nonempty, it contains some element @{term x}.  Since
   1.173 -it's closed under inverse, it contains @{text "(\<ominus>x)"}.  Since
   1.174 -it's closed under sum, it contains @{text "x \<oplus> (\<ominus>x) = \<zero>"}.
   1.175 -How impressive that the proof is automatic!*}
   1.176 -lemma (in group) zero_in_subset:
   1.177 -     "[| H <= carrier G; H \<noteq> {}; \<forall>a \<in> H. (\<ominus>a) \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<oplus> b \<in> H|]
   1.178 -      ==> \<zero> \<in> H"
   1.179 -by force
   1.180 -
   1.181 -text{*A characterization of subgroups*}
   1.182 -lemma (in group) subgroupI:
   1.183 -     "[| H <= carrier G;  H \<noteq> {};  
   1.184 -         !!a. a \<in> H ==> (\<ominus>a) \<in> H; 
   1.185 -         !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |] 
   1.186 -      ==> subgroup H G"
   1.187 -apply (insert prems) 
   1.188 -apply (simp add: group_def subgroup_def)
   1.189 -apply (simp add: semigroup_def group_axioms_def, clarify) 
   1.190 -apply (simp add: funcsetI subsetD [of H "carrier G"])
   1.191 -apply (blast intro: zero_in_subset)  
   1.192 -done
   1.193 -
   1.194 -
   1.195 -lemma subgroup_imp_subset: "subgroup H G  ==> H <= carrier G"
   1.196 -by (simp add: subgroup_def)
   1.197 -
   1.198 -lemma (in group) subgroup_sum_closed:
   1.199 -     "[| subgroup H G; x \<in> H; y \<in> H |] ==> x \<oplus> y \<in> H"
   1.200 -by (simp add: subgroup_def group_def semigroup_def Pi_def) 
   1.201 -
   1.202 -lemma (in group) subgroup_minus_closed:
   1.203 -     "[| subgroup H G; x \<in> H |] ==> (\<ominus>x) \<in> H"
   1.204 -by (simp add: subgroup_def group_def group_axioms_def Pi_def) 
   1.205 -
   1.206 -lemma (in group) subgroup_zero_closed: "subgroup H G ==> \<zero> \<in> H"
   1.207 -by (simp add: subgroup_def group_def group_axioms_def) 
   1.208 -
   1.209 -text{*Global declarations, in force outside the locale*}
   1.210 -declare semigroup.sum_closed [simp]
   1.211 -
   1.212 -declare group.zero_closed [iff]
   1.213 -    and group.minus_closed [simp]
   1.214 -    and group.left_minus [simp]
   1.215 -    and group.left_zero [simp]
   1.216 -    and group.right_minus [simp]
   1.217 -    and group.right_zero [simp]
   1.218 -    and group.minus_minus [simp]
   1.219 -
   1.220 -
   1.221 -lemma subgroup_imp_group: "subgroup H G ==> group G"
   1.222 -by (simp add: subgroup_def) 
   1.223 -
   1.224 -lemma subgroup_nonempty: "~ subgroup {} G"
   1.225 -by (blast dest: subgroup_imp_group group.subgroup_zero_closed)
   1.226 -
   1.227 -lemma subgroup_card_positive:
   1.228 -     "[| finite(carrier G); subgroup H G |] ==> 0 < card(H)"
   1.229 -apply (subgoal_tac "finite H")
   1.230 - prefer 2 apply (blast intro: finite_subset dest: subgroup_imp_subset)
   1.231 -apply (rule ccontr)
   1.232 -apply (simp add: card_0_eq subgroup_nonempty) 
   1.233 -done
   1.234 -
   1.235 -subsection{*Direct Product of Two Groups*}
   1.236 -
   1.237 -text{*We want to overload product for all algebraic structures.  But it is not
   1.238 -easy.  All of them are instances of the same type, namely @{text
   1.239 -carrier_field_type}, which the record declaration generates automatically.
   1.240 -Overloading requires distinct types.*}
   1.241 -
   1.242 -constdefs 
   1.243 -  ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
   1.244 -  "ProdGroup G G' ==
   1.245 -    (| carrier = carrier G \<times> carrier G',
   1.246 -       sum = (%(x, x') (y, y'). (sum G x y, sum G' x' y')),
   1.247 -       gminus = (%(x, y). (gminus G x, gminus G' y)),
   1.248 -       zero = (zero G, zero G') |)"
   1.249 -
   1.250 -syntax (xsymbols)
   1.251 -  ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
   1.252 -            (infixr "\<otimes>" 80)
   1.253 -
   1.254 -
   1.255 -lemma P_carrier: "(carrier (G\<otimes>G')) = ((carrier G) \<times> (carrier G'))"
   1.256 -by (simp add: ProdGroup_def)
   1.257 -
   1.258 -lemma P_sum: "sum (G\<otimes>G') = (%(x, x') (y, y'). (sum G x y, sum G' x' y'))"
   1.259 -by (simp add: ProdGroup_def)
   1.260 -
   1.261 -lemma P_minus: "(gminus (G\<otimes>G')) = (%(x, y). (gminus G x, gminus G' y))"
   1.262 -by (simp add: ProdGroup_def)
   1.263 -
   1.264 -lemma P_zero: "zero (G\<otimes>G') = (zero G, zero G')"
   1.265 -by (simp add: ProdGroup_def)
   1.266 -
   1.267 -lemma P_sum_funcset:
   1.268 -     "[|semigroup G; semigroup G'|] ==>
   1.269 -      sum(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
   1.270 -by (auto intro!: funcsetI 
   1.271 -         simp add: semigroup.sum_closed P_sum P_carrier)
   1.272 -
   1.273 -lemma P_minus_funcset: 
   1.274 -     "[|group G; group G'|] ==>
   1.275 -      gminus(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
   1.276 -by (auto intro!: funcsetI 
   1.277 -         simp add: group_def group.minus_closed P_minus P_carrier)
   1.278 -
   1.279 -theorem ProdGroup_is_group: "[|group G; group G'|] ==> group (G\<otimes>G')"
   1.280 -apply (rule group.intro)
   1.281 - apply (simp add: group_def)  
   1.282 - apply (rule semigroup.intro) 
   1.283 -  apply (simp add: group_def P_sum_funcset)  
   1.284 - apply (force simp add: ProdGroup_def semigroup.sum_assoc)
   1.285 -apply (rule group_axioms.intro) 
   1.286 -   apply (simp add: P_minus_funcset)  
   1.287 -  apply (simp add: ProdGroup_def group.zero_closed) 
   1.288 - apply (force simp add: ProdGroup_def group.left_minus) 
   1.289 -apply (force simp add: ProdGroup_def group.left_zero) 
   1.290 -done
   1.291 -
   1.292 -lemma ProdGroup_arity: "ProdGroup : Group \<rightarrow> Group \<rightarrow> Group"
   1.293 -by (auto intro!: funcsetI ProdGroup_is_group)
   1.294 -
   1.295 -subsection{*Homomorphisms on Groups and Semigroups*}
   1.296 -
   1.297 -constdefs
   1.298 -  hom :: "[('a,'c)semigroup_scheme, ('b,'d)semigroup_scheme] => ('a => 'b)set"
   1.299 -   "hom S S' ==
   1.300 -     {h. h \<in> carrier S -> carrier S' & 
   1.301 -	 (\<forall>x \<in> carrier S. \<forall>y \<in> carrier S. h(sum S x y) = sum S' (h x) (h y))}"
   1.302 -
   1.303 -lemma hom_semigroup:
   1.304 -     "semigroup S ==> semigroup (|carrier = hom S S, sum = (%h g. h o g) |)"
   1.305 -apply (simp add: semigroup_def o_assoc) 
   1.306 -apply (simp add: Pi_def hom_def) 
   1.307 -done
   1.308 -
   1.309 -lemma hom_sum:
   1.310 -     "[|h \<in> hom S S'; x \<in> carrier S; y \<in> carrier S|] 
   1.311 -      ==> h(sum S x y) = sum S' (h x) (h y)"
   1.312 -by (simp add: hom_def) 
   1.313 -
   1.314 -lemma hom_closed:
   1.315 -     "[|h \<in> hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
   1.316 -by (auto simp add: hom_def funcset_mem) 
   1.317 -
   1.318 -lemma hom_zero_closed [simp]:
   1.319 -     "[|h \<in> hom G G'; group G|] ==> h (zero G) \<in> carrier G'"
   1.320 -by (auto simp add: hom_closed) 
   1.321 -
   1.322 -text{*Or just @{text "group_hom.hom_zero [OF group_homI]"}*}
   1.323 -lemma hom_zero [simp]:
   1.324 -     "[|h \<in> hom G G'; group G; group G'|] ==> h (zero G) = zero G'"
   1.325 -by (simp add: group.idempotent_imp_zero hom_sum [of h, symmetric]) 
   1.326 -
   1.327 -lemma hom_minus_closed [simp]:
   1.328 -     "[|h \<in> hom G G'; x \<in> carrier G; group G|] 
   1.329 -      ==> h (gminus G x) \<in> carrier G'"
   1.330 -by (simp add: hom_closed) 
   1.331 -
   1.332 -text{*Or just @{text "group_hom.hom_minus [OF group_homI]"}*}
   1.333 -lemma hom_minus [simp]:
   1.334 -     "[|h \<in> hom G G'; x \<in> carrier G; group G; group G'|] 
   1.335 -      ==> h (gminus G x) = gminus G' (h x)"
   1.336 -by (simp add: group.minus_unique hom_closed hom_sum [of h, symmetric])
   1.337 -
   1.338 -
   1.339 -text{*This locale uses the subscript notation mentioned by Wenzel in 
   1.340 -@{text "HOL/ex/Locales.thy"}.  We fix two groups and a homomorphism between 
   1.341 -them.  Then we prove theorems similar to those just above.*}
   1.342 -
   1.343 -locale group_homomorphism = group G + group G' +
   1.344 -  fixes h
   1.345 -  assumes homh: "h \<in> hom G G'"
   1.346 -
   1.347 -lemma (in group_homomorphism) hom_sum [simp]:
   1.348 -     "[|x \<in> carrier G; y \<in> carrier G|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
   1.349 -by (simp add: hom_sum [OF homh])
   1.350 -
   1.351 -lemma (in group_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier G'"
   1.352 -by (simp add: hom_closed [OF homh]) 
   1.353 -
   1.354 -lemma (in group_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
   1.355 -by (simp add: idempotent_imp_zero hom_sum [symmetric]) 
   1.356 -
   1.357 -lemma (in group_homomorphism) hom_minus_closed [simp]:
   1.358 -     "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier G'"
   1.359 -by (simp add: hom_closed [OF homh]) 
   1.360 -
   1.361 -lemma (in group_homomorphism) hom_minus [simp]:
   1.362 -     "x \<in> carrier G ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
   1.363 -by (simp add: minus_unique hom_closed [OF homh] hom_sum [symmetric])
   1.364 -
   1.365 -text{*Necessary because the standard theorem
   1.366 -    @{text "group_homomorphism.intro"} is unnatural.*}
   1.367 -lemma group_homomorphismI:
   1.368 -    "[|group G; group G'; h \<in> hom G G'|] ==> group_homomorphism G G' h"
   1.369 -by (simp add: group_def group_homomorphism_def group_homomorphism_axioms_def)
   1.370 -
   1.371 -end
   1.372 - 
     2.1 --- a/src/HOL/GroupTheory/README.html	Mon May 05 18:23:40 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,40 +0,0 @@
     2.4 -<!-- $Id$ -->
     2.5 -<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
     2.6 -
     2.7 -<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
     2.8 -
     2.9 -<P>This directory presents proofs about group theory, by
    2.10 -Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
    2.11 -These theories use locales and were indeed the original motivation for
    2.12 -locales.  However, this treatment of groups must still be regarded as
    2.13 -experimental.  We can expect to see refinements in the future.
    2.14 -
    2.15 -Here is an outline of the directory's contents:
    2.16 -
    2.17 -<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
    2.18 -semigroups, groups, homomorphisms and the subgroup relation.  It also defines
    2.19 -the product of two groups.  It defines the factorization of a group and shows
    2.20 -that the factorization a normal subgroup is a group.
    2.21 -
    2.22 -<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
    2.23 -defines bijections over sets and operations on them and shows that they
    2.24 -are a group.  It shows that automorphisms form a group.
    2.25 -
    2.26 -<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
    2.27 -a few basic theorems.  Ring automorphisms are shown to form a group.
    2.28 -
    2.29 -<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
    2.30 -contains a proof of the first Sylow theorem.
    2.31 -
    2.32 -<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
    2.33 -abelian groups by a summation operator for finite sets (provided by
    2.34 -Clemens Ballarin).
    2.35 -</UL>
    2.36 -
    2.37 -<HR>
    2.38 -<P>Last modified on $Date$
    2.39 -
    2.40 -<ADDRESS>
    2.41 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    2.42 -</ADDRESS>
    2.43 -</BODY></HTML>
     3.1 --- a/src/HOL/GroupTheory/ROOT.ML	Mon May 05 18:23:40 2003 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,3 +0,0 @@
     3.4 -no_document use_thy "FuncSet";
     3.5 -
     3.6 -use_thy "Group";
     4.1 --- a/src/HOL/GroupTheory/document/root.tex	Mon May 05 18:23:40 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,26 +0,0 @@
     4.4 -\documentclass[a4paper]{article}
     4.5 -\usepackage{graphicx}
     4.6 -\usepackage{isabelle,isabellesym,pdfsetup}
     4.7 -\usepackage{amssymb,textcomp} %special symbols: old-style 0, 1, \lhd, ...
     4.8 -
     4.9 -\urlstyle{rm}
    4.10 -\isabellestyle{tt}
    4.11 -
    4.12 -\begin{document}
    4.13 -
    4.14 -\title{Fundamentals of Group Theory and Ring Theory}
    4.15 -\author{Florian Kamm{{\"u}}ller\\ Lawrence C Paulson}
    4.16 -\maketitle
    4.17 -
    4.18 -\tableofcontents
    4.19 -
    4.20 -\begin{center}
    4.21 -  \includegraphics[scale=0.7]{session_graph}  
    4.22 -\end{center}
    4.23 -
    4.24 -\newpage
    4.25 -
    4.26 -\parindent 0pt\parskip 0.5ex
    4.27 -\input{session}
    4.28 -
    4.29 -\end{document}