src/FOL/ex/NewLocaleTest.thy
2008-12-05 ballarin 2008-12-05 Interpretation in proof contexts.
2008-12-05 ballarin 2008-12-05 Interpretation in theories including interaction with subclass relation.
2008-12-01 ballarin 2008-12-01 No resolution of patterns within context statements.
2008-12-01 ballarin 2008-12-01 Methods intro_locales and unfold_locales apply to both old and new locales.
2008-11-28 ballarin 2008-11-28 Intro_locales_tac to simplify goals involving locale predicates.
2008-11-28 ballarin 2008-11-28 Perform higher-order pattern matching during round-up.
2008-11-27 ballarin 2008-11-27 Proper treatment of expressions with free arguments.
2008-11-27 ballarin 2008-11-27 Tests for sublocale command.
2008-11-25 ballarin 2008-11-25 Test for term patterns added.
2008-11-24 ballarin 2008-11-24 Some regression tests for theorem statements.
2008-11-21 ballarin 2008-11-21 Regression tests for new locale implementation.