src/HOL/UNITY/UNITY_Main.thy
changeset 32689 860e1a2317bd
parent 32149 ef59550a55d3
child 42767 e6d920bea7a6
     1.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 12:24:21 2009 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 14:23:04 2009 +0200
     1.3 @@ -1,13 +1,14 @@
     1.4  (*  Title:      HOL/UNITY/UNITY_Main.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   2003  University of Cambridge
     1.8  *)
     1.9  
    1.10  header{*Comprehensive UNITY Theory*}
    1.11  
    1.12 -theory UNITY_Main imports Detects PPROD Follows ProgressSets
    1.13 -uses "UNITY_tactics.ML" begin
    1.14 +theory UNITY_Main
    1.15 +imports Detects PPROD Follows ProgressSets
    1.16 +uses "UNITY_tactics.ML"
    1.17 +begin
    1.18  
    1.19  method_setup safety = {*
    1.20      Scan.succeed (fn ctxt =>