src/Pure/Isar/skip_proof.ML
2005-07-14 wenzelm 2005-07-14 tuned;
2005-04-23 wenzelm 2005-04-23 qualified name Pure.skip_proof;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-07 wenzelm 2005-04-07 Thm.invoke_oracle_i;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-28 wenzelm 2001-11-28 skip_proof: do not require quick_and_dirty in interactive mode;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-11 wenzelm 2001-11-11 adapted to multiple results;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-10-27 wenzelm 2001-10-27 added prove;
2001-10-22 wenzelm 2001-10-22 moved prove_goalw_cterm to goals.ML; cleaned up;
2001-10-12 wenzelm 2001-10-12 added make_thm (sort-of);
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-20 wenzelm 2000-03-20 added prove_goalw_cterm; quick_and_dirty moved here;
1999-07-12 wenzelm 1999-07-12 local qed; print rule;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;
1999-07-02 wenzelm 1999-07-02 skip_proof feature 'sorry' (for quick_and_dirty mode only);