# HG changeset patch
# User wenzelm
# Date 1007595619 -3600
# Node ID 2ba27248af7f89934fae60a18ab3d65c05ba9eb3
# Parent  9c27f28c8f5a73e2c803b8ed5dfeea33fa6039b3
tuned;

diff -r 9c27f28c8f5a -r 2ba27248af7f src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Thu Dec 06 00:40:04 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Thu Dec 06 00:40:19 2001 +0100
@@ -129,7 +129,7 @@
   also have "?a \<sqsubseteq> f ?a"
   proof
     from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
-    thus "f ?a : ?H" ..
+    thus "f ?a \<in> ?H" ..
   qed
   finally show "f ?a = ?a" .
 qed
diff -r 9c27f28c8f5a -r 2ba27248af7f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Dec 06 00:40:04 2001 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Dec 06 00:40:19 2001 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Library/Multiset.thy
     ID:         $Id$
-    Author:     Tobias Nipkow, TU Muenchen
-    Author:     Markus Wenzel, TU Muenchen
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {*
@@ -482,7 +481,7 @@
   {
     fix M M0 a
     assume M0: "M0 \<in> ?W"
-      and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+      and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
       and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
     have "M0 + {#a#} \<in> ?W"
     proof (rule accI [of "M0 + {#a#}"])
@@ -538,7 +537,7 @@
     from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
     proof induct
       fix a
-      assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+      assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
       show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
       proof
         fix M assume "M \<in> ?W"
diff -r 9c27f28c8f5a -r 2ba27248af7f src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:04 2001 +0100
+++ b/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:19 2001 +0100
@@ -14,7 +14,8 @@
   val netpair_bang: Proof.context -> netpair
   val netpair: Proof.context -> netpair
   val orderlist: ((int * int) * 'a) list -> 'a list
-  val find_rules: Proof.context -> thm list -> term -> thm list list
+  val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
+  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
   val print_global_rules: theory -> unit
   val print_local_rules: Proof.context -> unit
   val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
@@ -166,6 +167,8 @@
 val netpair = hd o tl o netpairs;
 
 
+(* retrieving rules *)
+
 fun untaglist [] = []
   | untaglist [(k : int * int, x)] = [x]
   | untaglist ((k, x) :: (rest as (k', x') :: _)) =
@@ -174,16 +177,22 @@
 
 fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
 fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
-fun may_unify t net = map snd (orderlist_no_weight (Net.unify_term net t));
+
+fun may_unify weighted t net =
+  map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
+
+fun find_erules _ [] = K []
+  | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
+fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
 
-fun find_erules [] = K []
-  | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
-fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
+fun find_rules_netpair weighted facts goal (inet, enet) =
+  find_erules weighted facts enet @ find_irules weighted goal inet;
 
-fun find_rules ctxt facts goal =
-  map (fn (inet, enet) => find_erules facts enet @ find_irules goal inet) (netpairs ctxt);
+fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
 
 
+(* wrappers *)
+
 fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
 
diff -r 9c27f28c8f5a -r 2ba27248af7f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Dec 06 00:40:04 2001 +0100
+++ b/src/Pure/Isar/method.ML	Thu Dec 06 00:40:19 2001 +0100
@@ -272,7 +272,7 @@
   let
     val rules =
       if not (null arg_rules) then arg_rules
-      else flat (ContextRules.find_rules ctxt facts goal)
+      else flat (ContextRules.find_rules false facts goal ctxt)
   in trace ctxt rules; tac rules facts i end);
 
 fun meth tac x = METHOD (HEADGOAL o tac x);