adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib/wp: Slight cleanup in WP-method.ML

This commit is contained in:
Thomas Sewell 2018-01-19 10:45:11 +11:00
parent be45b71fd7
commit 7bff086fef
1 changed files with 0 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
lib/Monad_WP/wp/WP-method.ML
View File

@ -16,10 +16,6 @@ sig
val debug_get: Proof.context -> wp_rules;
val derived_rule: thm -> thm -> thm list;
val get_combined_rules': thm list -> thm -> thm list;
val get_combined_rules: thm list -> thm list -> thm list;
val get_rules: Proof.context -> thm list -> wp_rules;
val apply_rules_tac_n: bool -> Proof.context -> thm list -> thm list Unsynchronized.ref
@ -127,18 +123,8 @@ let
val results = case get_key trip_conv thm of
SOME k => Net.lookup triples (Net.key_of_term k)
| NONE => others
in exists (fn (_, thm') => Thm.eq_thm_prop (thm, thm')) results end
fun derived_rule rule combinator =
[rule RSN (1, combinator)] handle THM _ => [];
fun get_combined_rules' combs' rule =
rule :: (List.concat (map (derived_rule rule) combs'));
fun get_combined_rules rules' combs' =
List.concat (map (get_combined_rules' combs') rules');
fun add_rule rule rs =
{trips = #trips rs,
rules = add_rule_inner (snd (#trips rs)) rule (#rules rs),