src/HOL/Tools/Meson/meson.ML
changeset 39953 aa54f347e5e2
parent 39950 f3c4849868b8
child 39979 b13515940b53
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 11:14:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 11:45:10 2010 +0200
     1.3 @@ -66,24 +66,24 @@
     1.4  val all_forward = @{thm all_forward};
     1.5  val ex_forward = @{thm ex_forward};
     1.6  
     1.7 -val not_conjD = @{thm meson_not_conjD};
     1.8 -val not_disjD = @{thm meson_not_disjD};
     1.9 -val not_notD = @{thm meson_not_notD};
    1.10 -val not_allD = @{thm meson_not_allD};
    1.11 -val not_exD = @{thm meson_not_exD};
    1.12 -val imp_to_disjD = @{thm meson_imp_to_disjD};
    1.13 -val not_impD = @{thm meson_not_impD};
    1.14 -val iff_to_disjD = @{thm meson_iff_to_disjD};
    1.15 -val not_iffD = @{thm meson_not_iffD};
    1.16 -val conj_exD1 = @{thm meson_conj_exD1};
    1.17 -val conj_exD2 = @{thm meson_conj_exD2};
    1.18 -val disj_exD = @{thm meson_disj_exD};
    1.19 -val disj_exD1 = @{thm meson_disj_exD1};
    1.20 -val disj_exD2 = @{thm meson_disj_exD2};
    1.21 -val disj_assoc = @{thm meson_disj_assoc};
    1.22 -val disj_comm = @{thm meson_disj_comm};
    1.23 -val disj_FalseD1 = @{thm meson_disj_FalseD1};
    1.24 -val disj_FalseD2 = @{thm meson_disj_FalseD2};
    1.25 +val not_conjD = @{thm not_conjD};
    1.26 +val not_disjD = @{thm not_disjD};
    1.27 +val not_notD = @{thm not_notD};
    1.28 +val not_allD = @{thm not_allD};
    1.29 +val not_exD = @{thm not_exD};
    1.30 +val imp_to_disjD = @{thm imp_to_disjD};
    1.31 +val not_impD = @{thm not_impD};
    1.32 +val iff_to_disjD = @{thm iff_to_disjD};
    1.33 +val not_iffD = @{thm not_iffD};
    1.34 +val conj_exD1 = @{thm conj_exD1};
    1.35 +val conj_exD2 = @{thm conj_exD2};
    1.36 +val disj_exD = @{thm disj_exD};
    1.37 +val disj_exD1 = @{thm disj_exD1};
    1.38 +val disj_exD2 = @{thm disj_exD2};
    1.39 +val disj_assoc = @{thm disj_assoc};
    1.40 +val disj_comm = @{thm disj_comm};
    1.41 +val disj_FalseD1 = @{thm disj_FalseD1};
    1.42 +val disj_FalseD2 = @{thm disj_FalseD2};
    1.43  
    1.44  
    1.45  (**** Operators for forward proof ****)
    1.46 @@ -212,7 +212,7 @@
    1.47  (*They are typically functional reflexivity axioms and are the converses of
    1.48    injectivity equivalences*)
    1.49  
    1.50 -val not_refl_disj_D = @{thm meson_not_refl_disj_D};
    1.51 +val not_refl_disj_D = @{thm not_refl_disj_D};
    1.52  
    1.53  (*Is either term a Var that does not properly occur in the other term?*)
    1.54  fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))