Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Minimal proof tuning.
authornipkow
Thu, 29 Jun 1995 10:43:07 +0200
changeset 1161 1831ba01c90c
parent 1160 8845eb5f0e5e
child 1162 7be0684950a3
Minimal proof tuning.
src/HOL/Lambda/Confluence.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/Confluence.ML	Mon Jun 26 14:34:19 1995 +0200
+++ b/src/HOL/Lambda/Confluence.ML	Thu Jun 29 10:43:07 1995 +0200
@@ -37,15 +37,10 @@
 goalw Confluence.thy [confluent_def,diamond_def,Church_Rosser_def]
   "Church_Rosser(R) = confluent(R)";
 br iffI 1;
- by(safe_tac HOL_cs);
- be allE 1;
- be allE 1;
- be mp 1;
- br rtrancl_trans 1;
-  br (Un_upper2 RS rtrancl_mono RS subsetD) 1;
-  br rtrancl_converseI 1;
-  be converseI 1;
- be (Un_upper1 RS rtrancl_mono RS subsetD) 1;
+ by(fast_tac (HOL_cs addIs
+      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
+       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
+by(safe_tac HOL_cs);
 be rtrancl_induct 1;
  by(fast_tac trancl_cs 1);
  by(slow_tac (rel_cs addIs [r_into_rtrancl]
isabelle