make-dist
author nipkow
Mon Apr 22 15:42:20 1996 +0200 (1996-04-22)
changeset 1669 e56cdf711729
parent 0 a5a9c433f639
permissions -rwxr-xr-x
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
clasohm@0
     1
#!/bin/sh
clasohm@0
     2
#make-dist <DIR> 
clasohm@0
     3
#make a distribution directory of Isabelle sources. Example:    
clasohm@0
     4
#    rm -r /usr/groups/theory/isabelle/91
clasohm@0
     5
#    make-dist /usr/groups/theory/isabelle/91
clasohm@0
     6
clasohm@0
     7
#BEFORE MAKING A NEW DISTRIBUTION VERSION, CHECK...
clasohm@0
     8
#   * that make-all works perfectly
clasohm@0
     9
#   * that README files are up-to-date
clasohm@0
    10
#   * that the version number has been updated
clasohm@0
    11
clasohm@0
    12
#This version copies EVERYTHING!!!!!!!!!!!!!!!!
clasohm@0
    13
clasohm@0
    14
set -e		#terminate if error
clasohm@0
    15
clasohm@0
    16
#Pure Isabelle
clasohm@0
    17
mkdir ${1?'No destination directory specified'}
clasohm@0
    18
cp -ipr . $1
clasohm@0
    19
clasohm@0
    20
#TO WRITE POLY/ML AND ISABELLE TAPES, USE SHELL SCRIPT write-dist
clasohm@0
    21
#TO PACK FOR EMAIL, USE SHELL SCRIPTS make-emaildist, send-emaildist