src/HOL/UNITY/UNITY_Main.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 32689 860e1a2317bd
child 42767 e6d920bea7a6
permissions -rw-r--r--
declare lex_prod_def [code del]
     1 (*  Title:      HOL/UNITY/UNITY_Main.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2003  University of Cambridge
     4 *)
     5 
     6 header{*Comprehensive UNITY Theory*}
     7 
     8 theory UNITY_Main
     9 imports Detects PPROD Follows ProgressSets
    10 uses "UNITY_tactics.ML"
    11 begin
    12 
    13 method_setup safety = {*
    14     Scan.succeed (fn ctxt =>
    15         SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
    16     "for proving safety properties"
    17 
    18 method_setup ensures_tac = {*
    19   Args.goal_spec -- Scan.lift Args.name_source >>
    20   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
    21 *} "for proving progress properties"
    22 
    23 end