src/HOL/UNITY/UNITY_Main.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32149 ef59550a55d3
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/UNITY/UNITY_Main.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2003  University of Cambridge
     5 *)
     6 
     7 header{*Comprehensive UNITY Theory*}
     8 
     9 theory UNITY_Main imports Detects PPROD Follows ProgressSets
    10 uses "UNITY_tactics.ML" begin
    11 
    12 method_setup safety = {*
    13     Scan.succeed (fn ctxt =>
    14         SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
    15     "for proving safety properties"
    16 
    17 method_setup ensures_tac = {*
    18   Args.goal_spec -- Scan.lift Args.name_source >>
    19   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
    20 *} "for proving progress properties"
    21 
    22 end