equal
deleted
inserted
replaced
128 fun meta_outer ctxt = |
128 fun meta_outer ctxt = |
129 curry_rule ctxt o Drule.export_without_context o |
129 curry_rule ctxt o Drule.export_without_context o |
130 rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
130 rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
131 |
131 |
132 (*Strip off the outer !P*) |
132 (*Strip off the outer !P*) |
133 val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; |
133 val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec; |
134 |
134 |
135 fun tracing true _ = () |
135 fun tracing true _ = () |
136 | tracing false msg = writeln msg; |
136 | tracing false msg = writeln msg; |
137 |
137 |
138 fun simplify_defn strict thy ctxt congs wfs id pats def0 = |
138 fun simplify_defn strict thy ctxt congs wfs id pats def0 = |