Added attribute rulify_prems (useful for modifying premises of introduction
authorberghofe
Tue Oct 05 15:29:46 1999 +0200 (1999-10-05)
changeset 7717e7ecfa617443
parent 7716 b0cb304517d4
child 7718 86755cc5b83c
Added attribute rulify_prems (useful for modifying premises of introduction
rules of inductive sets).
src/HOL/Set.ML
src/HOL/subset.thy
     1.1 --- a/src/HOL/Set.ML	Tue Oct 05 15:29:36 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Oct 05 15:29:46 1999 +0200
     1.3 @@ -745,3 +745,20 @@
     1.4  Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
     1.5  by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
     1.6  qed "subset_psubset_trans";
     1.7 +
     1.8 +
     1.9 +(* attributes *)
    1.10 +
    1.11 +local
    1.12 +
    1.13 +fun gen_rulify_prems x =
    1.14 +  Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
    1.15 +    rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
    1.16 +
    1.17 +in
    1.18 +
    1.19 +val rulify_prems_attrib_setup =
    1.20 + [Attrib.add_attributes
    1.21 +  [("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]];
    1.22 +
    1.23 +end;
     2.1 --- a/src/HOL/subset.thy	Tue Oct 05 15:29:36 1999 +0200
     2.2 +++ b/src/HOL/subset.thy	Tue Oct 05 15:29:46 1999 +0200
     2.3 @@ -7,4 +7,6 @@
     2.4  theory subset = Set
     2.5  files "Tools/typedef_package.ML":
     2.6  
     2.7 +setup rulify_prems_attrib_setup
     2.8 +
     2.9  end