src/HOL/UNITY/UNITY_Main.thy
changeset 32689 860e1a2317bd
parent 32149 ef59550a55d3
child 42767 e6d920bea7a6
--- 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 =>