| #
8ca82f10 |
|
02-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
| #
1a9510ea |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
744c494f |
|
27-Jun-2013 |
wenzelm <none@none> |
tuned signature;
|
| #
c80e2d62 |
|
30-May-2013 |
wenzelm <none@none> |
tuned signature;
|
| #
afb3cb3a |
|
30-May-2013 |
wenzelm <none@none> |
tuned signature;
tuned;
|
| #
1c4fa991 |
|
30-May-2013 |
wenzelm <none@none> |
misc tuning;
|
| #
530afa9e |
|
30-May-2013 |
wenzelm <none@none> |
more standard fold/fold_rev;
|
| #
011deaf5 |
|
12-Sep-2012 |
wenzelm <none@none> |
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
|
| #
7e6b72a0 |
|
12-Sep-2012 |
wenzelm <none@none> |
eliminated some old material that is unused in the visible universe;
|
| #
24c076f3 |
|
03-Mar-2012 |
wenzelm <none@none> |
tuned;
|
| #
ab54c3b1 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
| #
68ed89ae |
|
10-Aug-2011 |
wenzelm <none@none> |
old term operations are legacy;
|
| #
ec1196d6 |
|
09-Jun-2011 |
wenzelm <none@none> |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
| #
bbc8cf56 |
|
20-Mar-2010 |
wenzelm <none@none> |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
| #
d62b04dd |
|
06-Jul-2009 |
wenzelm <none@none> |
structure Thm: less pervasive names;
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
| #
1be33ad4 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
| #
b88342b6 |
|
30-Dec-2008 |
wenzelm <none@none> |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
| #
d4aa0c76 |
|
15-Apr-2008 |
wenzelm <none@none> |
Thm.forall_elim_var(s);
|
| #
4e29e34b |
|
31-May-2007 |
wenzelm <none@none> |
tuned headers -- adapted to usual conventions;
|
| #
2907ad77 |
|
31-May-2007 |
wenzelm <none@none> |
moved IsaPlanner from Provers to Tools;
|