src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg
author oheimb
Fri, 13 Dec 1996 18:32:07 +0100
changeset 2392 2fb9659d30ca
parent 1830 861736a24a93
permissions -rw-r--r--
minor adaptions

Configuration file for extracting the 8bit patches from Isabelle

STEM "/usr/wiss/oheimb/isabelle/"

EXTRACT Tools/8bit/isa-patches/HOL/HOL1.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
EXTRACT Tools/8bit/isa-patches/HOL/HOL2.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
EXTRACT Tools/8bit/isa-patches/HOL/Set.p IN HOL/Set.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
EXTRACT Tools/8bit/isa-patches/HOL/Prod.p IN HOL/Prod.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
EXTRACT Tools/8bit/isa-patches/HOL/Nat.p IN HOL/Nat.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"