src/HOL/LOrder.thy
changeset 17508 c84af7f39a6b
parent 15524 2ef571f80a55
child 21213 c81f016883df
     1.1 --- a/src/HOL/LOrder.thy	Tue Sep 20 13:58:58 2005 +0200
     1.2 +++ b/src/HOL/LOrder.thy	Tue Sep 20 14:03:37 2005 +0200
     1.3 @@ -285,48 +285,4 @@
     1.4    from b c show ?thesis by (simp add: meet_imp_le)
     1.5  qed
     1.6  
     1.7 -ML {*
     1.8 -val is_meet_unique = thm "is_meet_unique";
     1.9 -val is_join_unique = thm "is_join_unique";
    1.10 -val join_exists = thm "join_exists";
    1.11 -val meet_exists = thm "meet_exists";
    1.12 -val is_meet_meet = thm "is_meet_meet";
    1.13 -val meet_unique = thm "meet_unique";
    1.14 -val is_join_join = thm "is_join_join";
    1.15 -val join_unique = thm "join_unique";
    1.16 -val meet_left_le = thm "meet_left_le";
    1.17 -val meet_right_le = thm "meet_right_le";
    1.18 -val meet_imp_le = thm "meet_imp_le";
    1.19 -val join_left_le = thm "join_left_le";
    1.20 -val join_right_le = thm "join_right_le";
    1.21 -val join_imp_le = thm "join_imp_le";
    1.22 -val meet_join_le = thms "meet_join_le";
    1.23 -val is_meet_min = thm "is_meet_min";
    1.24 -val is_join_max = thm "is_join_max";
    1.25 -val meet_min = thm "meet_min";
    1.26 -val join_max = thm "join_max";
    1.27 -val meet_idempotent = thm "meet_idempotent";
    1.28 -val join_idempotent = thm "join_idempotent";
    1.29 -val meet_comm = thm "meet_comm";
    1.30 -val join_comm = thm "join_comm";
    1.31 -val meet_assoc = thm "meet_assoc";
    1.32 -val join_assoc = thm "join_assoc";
    1.33 -val meet_left_comm = thm "meet_left_comm";
    1.34 -val meet_left_idempotent = thm "meet_left_idempotent";
    1.35 -val join_left_comm = thm "join_left_comm";
    1.36 -val join_left_idempotent = thm "join_left_idempotent";
    1.37 -val meet_aci = thms "meet_aci";
    1.38 -val join_aci = thms "join_aci";
    1.39 -val le_def_meet = thm "le_def_meet";
    1.40 -val le_def_join = thm "le_def_join";
    1.41 -val meet_join_absorp = thm "meet_join_absorp";
    1.42 -val join_meet_absorp = thm "join_meet_absorp";
    1.43 -val meet_mono = thm "meet_mono";
    1.44 -val join_mono = thm "join_mono";
    1.45 -val distrib_join_le = thm "distrib_join_le";
    1.46 -val distrib_meet_le = thm "distrib_meet_le";
    1.47 -val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
    1.48 -val modular_le = thm "modular_le";
    1.49 -*}
    1.50 -
    1.51  end