src/Tools/8bit/xmosaic/isa_xmosaic
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1826 2a2c0dbeb4ac
child 2852 ddb85eb8385f
permissions -rwxr-xr-x
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

#!/bin/bash
################################################
# Title:      Tools/8bit/xmosaic/isa_xmosaic
# ID:         $Id$
# Author:     Franz Regensburger
# Copyright   1995 TU Muenchen
#
# open xmosaic with isabelle font
#
# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 20.12.95
# 
###############################################
#
# The script is configured by the master makefile ../Makefile.
# Edit this file to make changes!
#

###############################################
# do not edit below
###############################################

ISAXMOSAICDIR=$ISABELLE8BIT/xmosaic

# start xmosaic ; 

xmosaic  -title "isa_xmosaic"  -xrm "\
Mosaic*font:isacr14" -xrm "\
Mosaic*fixedFont:isacr14" -xrm "\
Mosaic*plainFont:isacr14"