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.
provide case names for rev_induct, rev_cases;
authorwenzelm
Fri, 03 Nov 2000 21:33:15 +0100
changeset 10386 581a5a143994
parent 10385 22836e4c5f4e
child 10387 9dac2cad5500
provide case names for rev_induct, rev_cases;
src/HOL/Main.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Main.thy	Fri Nov 03 21:32:41 2000 +0100
+++ b/src/HOL/Main.thy	Fri Nov 03 21:33:15 2000 +0100
@@ -7,5 +7,7 @@
 (*belongs to theory List*)
 declare lists_mono [mono]
 declare map_cong [recdef_cong]
+lemmas rev_induct [case_names Nil snoc] = rev_induct
+  and rev_cases [case_names Nil snoc] = rev_exhaust
 
 end
isabelle