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.
theorems case_split = case_split_thm [case_names True False, cases type: o];
authorwenzelm
Fri, 09 Nov 2001 22:50:32 +0100
changeset 12127 219e543496a3
parent 12126 34f72eb7d2db
child 12128 25565bbbd246
theorems case_split = case_split_thm [case_names True False, cases type: o];
src/FOL/FOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL.thy	Fri Nov 09 10:26:16 2001 +0100
+++ b/src/FOL/FOL.thy	Fri Nov 09 22:50:32 2001 +0100
@@ -20,7 +20,7 @@
 subsection {* Lemmas and proof tools *}
 
 use "FOL_lemmas1.ML"
-theorems case_split = case_split_thm [case_names True False]
+theorems case_split = case_split_thm [case_names True False, cases type: o]
 
 use "cladata.ML"
 setup Cla.setup
isabelle