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.
Changed to use split instead of fsplit. The weakening of fsplitE appears not
authorlcp
Thu, 04 May 1995 02:02:18 +0200
changeset 1109 380e9eb40db7
parent 1108 22b256c8c9fb
child 1110 756aa2e81f6e
Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.
src/ZF/add_ind_def.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/add_ind_def.ML	Thu May 04 02:01:49 1995 +0200
+++ b/src/ZF/add_ind_def.ML	Thu May 04 02:02:18 1995 +0200
@@ -45,7 +45,7 @@
   val split_eq	: thm			(*equality rule for split*)
   val fsplitI	: thm			(*intro rule for fsplit*)
   val fsplitD	: thm			(*destruct rule for fsplit*)
-  val fsplitE	: thm			(*elim rule for fsplit*)
+  val fsplitE	: thm			(*elim rule; apparently never used*)
   end;
 
 signature SU =			(** Description of a disjoint sum **)
isabelle