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 if_bool_eq to if_bool_eq_conj
authorpaulson
Thu, 02 Apr 1998 13:48:48 +0200
changeset 4770 3e026ace28da
parent 4769 bb60149fe21b
child 4771 f1bacbbe02a8
changed if_bool_eq to if_bool_eq_conj
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.ML	Thu Apr 02 13:48:28 1998 +0200
+++ b/src/HOL/Set.ML	Thu Apr 02 13:48:48 1998 +0200
@@ -654,7 +654,7 @@
 bind_thm ("expand_if_mem2", 
     read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
 
-val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2,
+val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2,
 		  expand_if_mem1, expand_if_mem2];
isabelle