Complete Redesign of Theory, main points are:
- Extension of the continuity prover:
* Lemmas about continuity of flift1 and flift2 are generalized
* Lemmas about continuity of mixed definitions of HOL and LCF terms generalized
Pay attention: Sometimes proofs are shorter now!
- a number of new lemmas concerning flift1, flift2, Def and Undef,
Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2
are added to !simpset
Pay attention: Sometimes proofs are shorter now!
- added tactic def_tac for eliminating x~=UU in assumptions
#!/bin/sh
#make-dist <DIR>
#make a distribution directory of Isabelle sources. Example:
# rm -r /usr/groups/theory/isabelle/91
# make-dist /usr/groups/theory/isabelle/91
#BEFORE MAKING A NEW DISTRIBUTION VERSION, CHECK...
# * that make-all works perfectly
# * that README files are up-to-date
# * that the version number has been updated
#This version copies EVERYTHING!!!!!!!!!!!!!!!!
set -e #terminate if error
#Pure Isabelle
mkdir ${1?'No destination directory specified'}
cp -ipr . $1
#TO WRITE POLY/ML AND ISABELLE TAPES, USE SHELL SCRIPT write-dist
#TO PACK FOR EMAIL, USE SHELL SCRIPTS make-emaildist, send-emaildist