equal
deleted
inserted
replaced
140 |
140 |
141 val not_refl_disj_D = thm"meson_not_refl_disj_D"; |
141 val not_refl_disj_D = thm"meson_not_refl_disj_D"; |
142 |
142 |
143 fun refl_clause_aux 0 th = th |
143 fun refl_clause_aux 0 th = th |
144 | refl_clause_aux n th = |
144 | refl_clause_aux n th = |
145 (debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); |
145 (Output.debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); |
146 case HOLogic.dest_Trueprop (concl_of th) of |
146 case HOLogic.dest_Trueprop (concl_of th) of |
147 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => |
147 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => |
148 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) |
148 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) |
149 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => |
149 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => |
150 if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*) |
150 if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*) |