author | wenzelm |
Thu, 12 May 2011 18:18:06 +0200 | |
changeset 42767 | e6d920bea7a6 |
parent 32689 | 860e1a2317bd |
child 42795 | 66fcc9882784 |
permissions | -rw-r--r-- |
13786 | 1 |
(* Title: HOL/UNITY/UNITY_Main.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 2003 University of Cambridge |
|
13798 | 4 |
*) |
13786 | 5 |
|
13798 | 6 |
header{*Comprehensive UNITY Theory*} |
13786 | 7 |
|
32689 | 8 |
theory UNITY_Main |
9 |
imports Detects PPROD Follows ProgressSets |
|
10 |
uses "UNITY_tactics.ML" |
|
11 |
begin |
|
13786 | 12 |
|
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15032
diff
changeset
|
13 |
method_setup safety = {* |
42767 | 14 |
Scan.succeed (SIMPLE_METHOD' o constrains_tac) *} |
13786 | 15 |
"for proving safety properties" |
16 |
||
17 |
method_setup ensures_tac = {* |
|
30549 | 18 |
Args.goal_spec -- Scan.lift Args.name_source >> |
42767 | 19 |
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
30549 | 20 |
*} "for proving progress properties" |
13786 | 21 |
|
22 |
end |