--- a/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 12:24:21 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 14:23:04 2009 +0200
@@ -1,13 +1,14 @@
(* Title: HOL/UNITY/UNITY_Main.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
*)
header{*Comprehensive UNITY Theory*}
-theory UNITY_Main imports Detects PPROD Follows ProgressSets
-uses "UNITY_tactics.ML" begin
+theory UNITY_Main
+imports Detects PPROD Follows ProgressSets
+uses "UNITY_tactics.ML"
+begin
method_setup safety = {*
Scan.succeed (fn ctxt =>