added Clarify_tac to speed up proofs
authorpaulson
Mon Oct 19 11:26:46 1998 +0200 (1998-10-19)
changeset 5669f5d9caafc3bd
parent 5668 9ddc4e836d3e
child 5670 5e7d9455de96
added Clarify_tac to speed up proofs
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:25:37 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:26:46 1998 +0200
     1.3 @@ -170,6 +170,7 @@
     1.4  Goalw [Constrains_def, constrains_def]
     1.5     "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
     1.6  \   ==> F : Constrains A (A' Un B')";
     1.7 +by (Clarify_tac 1);
     1.8  by (Blast_tac 1);
     1.9  qed "Constrains_cancel";
    1.10  
     2.1 --- a/src/HOL/UNITY/UNITY.ML	Mon Oct 19 11:25:37 1998 +0200
     2.2 +++ b/src/HOL/UNITY/UNITY.ML	Mon Oct 19 11:26:46 1998 +0200
     2.3 @@ -224,6 +224,7 @@
     2.4  Goalw [constrains_def]
     2.5     "[| F : constrains A (A' Un B); F : constrains B B' |] \
     2.6  \   ==> F : constrains A (A' Un B')";
     2.7 +by (Clarify_tac 1);
     2.8  by (Blast_tac 1);
     2.9  qed "constrains_cancel";
    2.10  
     3.1 --- a/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:25:37 1998 +0200
     3.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:26:46 1998 +0200
     3.3 @@ -421,6 +421,7 @@
     3.4  \      F : constrains (A1 - B) (A1 Un B); \
     3.5  \      F : constrains (A2 - C) (A2 Un C) |] \
     3.6  \   ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
     3.7 +by (Clarify_tac 1);
     3.8  by (Blast_tac 1);
     3.9  val lemma1 = result();
    3.10