src/HOL/Tools/meson.ML
changeset 31454 2c0959ab073f
parent 30607 c3d1590debd8
child 31945 d5f186aa0bed
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Jun 04 15:28:58 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jun 04 15:28:58 2009 +0200
     1.3 @@ -46,6 +46,19 @@
     1.4  val max_clauses_default = 60;
     1.5  val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
     1.6  
     1.7 +val disj_forward = @{thm disj_forward};
     1.8 +val disj_forward2 = @{thm disj_forward2};
     1.9 +val make_pos_rule = @{thm make_pos_rule};
    1.10 +val make_pos_rule' = @{thm make_pos_rule'};
    1.11 +val make_pos_goal = @{thm make_pos_goal};
    1.12 +val make_neg_rule = @{thm make_neg_rule};
    1.13 +val make_neg_rule' = @{thm make_neg_rule'};
    1.14 +val make_neg_goal = @{thm make_neg_goal};
    1.15 +val conj_forward = @{thm conj_forward};
    1.16 +val all_forward = @{thm all_forward};
    1.17 +val ex_forward = @{thm ex_forward};
    1.18 +val choice = @{thm choice};
    1.19 +
    1.20  val not_conjD = thm "meson_not_conjD";
    1.21  val not_disjD = thm "meson_not_disjD";
    1.22  val not_notD = thm "meson_not_notD";