src/Cube/Example.thy
2016-01-01 wenzelm 2016-01-01 isabelle update_cartouches -c -t;
2015-10-10 wenzelm 2015-10-10 tuned whitespace;
2015-10-10 wenzelm 2015-10-10 tuned;
2015-10-10 wenzelm 2015-10-10 tuned syntax -- more symbols;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-02-10 wenzelm 2015-02-10 misc tuning;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-07 wenzelm 2014-10-07 more cartouches;
2011-10-22 wenzelm 2011-10-22 discontinued redundant ASCII syntax;
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2006-06-22 ballarin 2006-06-22 Removed debugging code.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-09-17 wenzelm 2005-09-17 plain test session, includes example;