aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-09-19 09:44:04 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-09-19 09:44:04 +0000
commit1ae6f0640e03d7375c5585c77fc6df9d1ab0630e (patch)
tree57d8700a90d1588fe3ff3482c6f5a48c28eccf0f /generic
parent41113572f109f81db301aab9ed828cb60438c4c8 (diff)
isa: DEFAULT_FILES="Scratch.thy Scratch.ML";
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions