equal
deleted
inserted
replaced
8 (** tools setup **) |
8 (** tools setup **) |
9 |
9 |
10 structure Quantifier1 = Quantifier1 |
10 structure Quantifier1 = Quantifier1 |
11 ( |
11 ( |
12 (*abstract syntax*) |
12 (*abstract syntax*) |
13 fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t) |
13 fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t) |
14 | dest_eq _ = NONE; |
14 | dest_eq _ = NONE; |
15 fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t) |
15 fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t) |
16 | dest_conj _ = NONE; |
16 | dest_conj _ = NONE; |
17 fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t) |
17 fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t) |
18 | dest_imp _ = NONE; |
18 | dest_imp _ = NONE; |
19 val conj = HOLogic.conj |
19 val conj = HOLogic.conj |
20 val imp = HOLogic.imp |
20 val imp = HOLogic.imp |
21 (*rules*) |
21 (*rules*) |
22 val iff_reflection = @{thm eq_reflection} |
22 val iff_reflection = @{thm eq_reflection} |