# HG changeset patch # User wenzelm # Date 1188663456 -7200 # Node ID 540eaf87e42dbebb7402eee7aeb90447ad41c720 # Parent f39e79334052442caae815d710aae5654fc21faa mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings; diff -r f39e79334052 -r 540eaf87e42d src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sat Sep 01 16:12:50 2007 +0200 +++ b/src/HOL/Lattices.thy Sat Sep 01 18:17:36 2007 +0200 @@ -513,11 +513,15 @@ lemmas [code func del] = inf_set_eq sup_set_eq -lemmas mono_Int = mono_inf - [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq] +lemma mono_Int: "mono f \ f (A \ B) \ f A \ f B" + apply (fold inf_set_eq sup_set_eq) + apply (erule mono_inf) + done -lemmas mono_Un = mono_sup - [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq] +lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)" + apply (fold inf_set_eq sup_set_eq) + apply (erule mono_sup) + done instance set :: (type) complete_lattice Inf_set_def: "Inf S \ \S" @@ -581,9 +585,4 @@ lemmas inf_aci = inf_ACI lemmas sup_aci = sup_ACI -ML {* -val sup_fun_eq = @{thm sup_fun_eq} -val sup_bool_eq = @{thm sup_bool_eq} -*} - end