src/HOL/Makefile
changeset 2235 866dbb04816c
parent 2117 292df12bace5
child 2274 1b1b46adc9b3
     1.1 --- a/src/HOL/Makefile	Tue Nov 26 17:49:25 1996 +0100
     1.2 +++ b/src/HOL/Makefile	Wed Nov 27 10:31:05 1996 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4  			$(BIN) is the Isabelle source directory; \
     1.5  			exit 1; \
     1.6  	fi
     1.7 -	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
     1.8 +	@case `basename "$(COMP)"` in \
     1.9  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
    1.10  		  | $(COMP) $(BIN)/Pure;\
    1.11  		if [ "$${MAKE_HTML}" = "true" ]; \
    1.12 @@ -68,12 +68,13 @@
    1.13  #### Testing of HOL
    1.14  
    1.15  #A macro referring to the object-logic (depends on ML compiler)
    1.16 -LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
    1.17 -	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
    1.18 -	sml*)	echo "$ISABELLEBIN/HOL" ;;\
    1.19 +#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
    1.20 +LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
    1.21 +	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
    1.22 +	sml*)	echo "$(ISABELLEBIN)/HOL" ;;\
    1.23  	*)	echo "echo; echo Bad value for ISABELLECOMP: \
    1.24 -			$ISABELLECOMP is not poly or sml; exit 1" ;;\
    1.25 -	esac
    1.26 +			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
    1.27 +	esac`
    1.28  
    1.29  ##IMP-semantics example
    1.30  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.31 @@ -197,8 +198,8 @@
    1.32  	fi
    1.33  
    1.34  ##Miscellaneous examples
    1.35 -EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
    1.36 -	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
    1.37 +EX_NAMES = String BT Perm Comb InSort Qsort LexProd Group Ring Lagrange \
    1.38 +	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
    1.39  
    1.40  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.41  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)