aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-29 22:45:08 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-29 22:45:08 +0000
commitd02398289ff7cad3ae0f77a02273a17dc5c99b8d (patch)
treeb42f0ff9aa0733f42a0eace4c5d3e0d323f1029b /etc
parent2232a44c0151d0aeb5405990d6bf9548b6174ffc (diff)
Updated.
Diffstat (limited to 'etc')
-rw-r--r--etc/isar/trace_simp.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy
index 4788262c..06458a84 100644
--- a/etc/isar/trace_simp.thy
+++ b/etc/isar/trace_simp.thy
@@ -1,6 +1,6 @@
(* This is a test of tracing output for Isabelle. *)
-theory trace_simp = Main:
+theory trace_simp imports Main begin
text {*
this produces massive amount of simplifier trace, but terminates