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.
declare trancl rules;
authorwenzelm
Mon, 23 Oct 2000 22:12:04 +0200
changeset 10312 4c5a03649af7
parent 10311 3b53ed2c846f
child 10313 51e830bb7abe
declare trancl rules;
src/HOL/Inductive.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Inductive.thy	Mon Oct 23 22:11:43 2000 +0200
+++ b/src/HOL/Inductive.thy	Mon Oct 23 22:12:04 2000 +0200
@@ -18,11 +18,17 @@
 setup DatatypePackage.setup
 setup PrimrecPackage.setup
 
-theorems [mono] =
+theorems basic_monos [mono] =
    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
    Collect_mono in_mono vimage_mono
    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    not_all not_ex
    Ball_def Bex_def
 
+(*belongs to theory Transitive_Closure*)
+declare rtrancl_induct [induct set: rtrancl]
+declare rtranclE [cases set: rtrancl]
+declare trancl_induct [induct set: trancl]
+declare tranclE [cases set: trancl]
+
 end
isabelle