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
#!/bin/sh
# Title: make-rulenames
# Author: Larry Paulson, Cambridge University Computer Laboratory
# Copyright 1990 University of Cambridge
#
#shell script for adding signature and val declarations to a rules file
# usage: make-rulenames <directory>
#
#Input is the file ruleshell.ML, which defines a theory.
#Output is .rules.ML
#
#
#Rule lines begin with a line containing the word "extend_theory"
# and end with a line containing the word "get_axiom"
#
#Each rule name xyz must appear on a line that begins
# <spaces> ("xyz"
# ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER!
#The file RULESIG gets lines like val Eq_comp: thm
# These are inserted after the line containing the string INSERT-RULESIG
#
#The file RULENAMES gets lines like val Eq_comp = ax"Eq_comp";
# These are inserted after the line containing the string INSERT-RULENAMES
#The input file should define the function "ax" above this point.
#
set -eu #terminate if error or unset variable
if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \
then echo $1 is not a suitable directory; exit 1; \
fi
sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/ val \1: thm/p' $1/ruleshell.ML > RULESIG
sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES
sed -e '/INSERT-RULESIG/ r RULESIG
/INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML
#WARNING: there must be no spaces after the filename in the "r" command!!
rm RULESIG RULENAMES