EMAILDIST-README
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 0 a5a9c433f639
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
ISABELLE -- INSTRUCTIONS FOR UNPACKING THE EMAIL DISTRIBUTION 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
The Isabelle email distribution consists of about 8 installments, each
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
small enough to send by electronic mail.  The files are called Isabelle.aa,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
Isabelle.ab, ....  They have been generated by tar, compress, uuencode, and
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
split, and are packed for email using shar.  To unpack the files, perform
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
the following steps:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
STEP 1.  Create a new directory to hold Isabelle and move to that
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
directory (the name of the directory does not matter):
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
	mkdir Isabelle;  cd Isabelle
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
STEP 2.  Put each message into a separate file and pipe it through unshar.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(If you don't have unshar, remove the header lines generated by the mail
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
system and submit the file to sh.)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
STEP 3.  Concatenate the files into one file using the command
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
	cat Isabelle.?? > 92.tar.Z.uu
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
STEP 4.  Undo the uuencode operation using the command
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
	uudecode 92.tar.Z.uu
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
STEP 5.  You should now have a file 92.tar.Z; uncompress and unpack it using...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
   	uncompress -c 92.tar.Z | tar xf -
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
STEP 6.  You should now have a complete Isabelle directory, called 92.  You
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
may now tidy up by executing
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
	rm Isabelle.?? *.hdr 92.tar.Z.uu 92.tar.Z
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
Consult the file 92/README for information on compiling Isabelle.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
						Good luck!