src/HOL/Tools/meson.ML
changeset 20288 8ff4a0ea49b2
parent 20134 73cb53843190
child 20361 1aaf9ebe248d
equal deleted inserted replaced
20287:8cbcb46c3c09 20288:8ff4a0ea49b2
   449     REPEAT o (etac exE);
   449     REPEAT o (etac exE);
   450 
   450 
   451 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   451 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   452 fun expand_defs_tac st =
   452 fun expand_defs_tac st =
   453   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   453   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   454   in  LocalDefs.def_export false defs st  end;
   454   in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
   455 
   455 
   456 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   456 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   457 fun MESON cltac i st = 
   457 fun MESON cltac i st = 
   458   SELECT_GOAL
   458   SELECT_GOAL
   459     (EVERY [rtac ccontr 1,
   459     (EVERY [rtac ccontr 1,