| 2011-10-28 |
wenzelm |
2011-10-28 |
slightly more explicit/syntactic modelling of morphisms;
|
file | diff | annotate |
| 2011-07-12 |
wenzelm |
2011-07-12 |
more thorough Variable.check_name: Binding.check for logical entities within the term language;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
tuned signature: Name.invent and Name.invent_names;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
simplified Name.variant -- discontinued builtin fold_map;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
tuned signature -- eliminated odd comment;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
more informative markup for fixed variables (via name space entry);
uniform markup for undeclared entities;
tuned;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
reorganized fixes as specialized (global) name space;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
more uniform Variable.add_frees/add_fixed etc.;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
modernized structure Proof_Context;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
tuned signature, disentangled dependencies;
|
file | diff | annotate |
| 2010-10-25 |
wenzelm |
2010-10-25 |
recovered some odd two-dimensional layout;
|
file | diff | annotate |
| 2010-09-24 |
wenzelm |
2010-09-24 |
modernized structure Ord_List;
|
file | diff | annotate |
| 2010-09-12 |
wenzelm |
2010-09-12 |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
|
file | diff | annotate |
| 2010-08-27 |
wenzelm |
2010-08-27 |
more careful treatment of context visibility flag wrt. spurious warnings;
|
file | diff | annotate |
| 2010-05-27 |
wenzelm |
2010-05-27 |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| 2010-05-04 |
wenzelm |
2010-05-04 |
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-04-30 |
wenzelm |
2010-04-30 |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2009-11-25 |
haftmann |
2009-11-25 |
normalized uncurry take/drop
|
file | diff | annotate |
| 2009-11-24 |
haftmann |
2009-11-24 |
curried take/drop
|
file | diff | annotate |
| 2009-11-08 |
wenzelm |
2009-11-08 |
adapted Generic_Data, Proof_Data;
tuned;
|
file | diff | annotate |
| 2009-10-21 |
haftmann |
2009-10-21 |
curried inter as canonical list operation (beware of argument order)
|
file | diff | annotate |
| 2009-10-21 |
haftmann |
2009-10-21 |
dropped redundant gen_ prefix
|
file | diff | annotate |
| 2009-10-20 |
haftmann |
2009-10-20 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
eliminated redundant bindings;
|
file | diff | annotate |
| 2009-07-30 |
wenzelm |
2009-07-30 |
Variable.importT/import: return full instantiations, tuned;
|
file | diff | annotate |
| 2009-07-26 |
wenzelm |
2009-07-26 |
Variable.focus: named parameters;
|
file | diff | annotate |
| 2009-07-09 |
wenzelm |
2009-07-09 |
renamed structure TermSubst to Term_Subst;
|
file | diff | annotate |
| 2009-06-24 |
wenzelm |
2009-06-24 |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);
|
file | diff | annotate |
| 2009-03-28 |
wenzelm |
2009-03-28 |
replaced add_binds by singleton bind_term;
|
file | diff | annotate |
| 2009-01-21 |
wenzelm |
2009-01-21 |
eliminated obsolete var morphism;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
Term.declare_typ_names, Term.declare_term_frees;
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-10-16 |
wenzelm |
2008-10-16 |
maintain sort occurrences of declared terms;
|
file | diff | annotate |
| 2008-06-19 |
wenzelm |
2008-06-19 |
added declare_typ;
|
file | diff | annotate |
| 2008-06-10 |
wenzelm |
2008-06-10 |
focus: actually declare constraints for local parameters;
|
file | diff | annotate |
| 2008-04-17 |
wenzelm |
2008-04-17 |
variant_fixes: preserve internal state, mark skolem only for body mode;
import_inst: actually observe is_open flag (cf. variant_fixes);
|
file | diff | annotate |
| 2007-12-07 |
haftmann |
2007-12-07 |
exported declare_names
|
file | diff | annotate |
| 2007-11-07 |
wenzelm |
2007-11-07 |
refined notion of consts within the local scope;
|
file | diff | annotate |
| 2007-11-06 |
wenzelm |
2007-11-06 |
added is_const/declare_const for local scope of fixes/consts;
|
file | diff | annotate |
| 2007-10-16 |
wenzelm |
2007-10-16 |
add_bind: close_schematic_term;
|
file | diff | annotate |
| 2007-10-04 |
wenzelm |
2007-10-04 |
replaced literal 'a by Name.aT;
|
file | diff | annotate |
| 2007-09-29 |
wenzelm |
2007-09-29 |
maintain maxidx (analogous to name context);
polymorhic: observe Variable.maxidx_of;
|
file | diff | annotate |
| 2007-09-26 |
wenzelm |
2007-09-26 |
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
|
file | diff | annotate |
| 2007-09-24 |
wenzelm |
2007-09-24 |
added polymorphic_types;
|
file | diff | annotate |
| 2007-05-07 |
wenzelm |
2007-05-07 |
simplified DataFun interfaces;
|
file | diff | annotate |
| 2007-04-15 |
wenzelm |
2007-04-15 |
removed obsolete redeclare_skolems;
|
file | diff | annotate |
| 2007-04-15 |
wenzelm |
2007-04-15 |
Thm.fold_terms;
|
file | diff | annotate |
| 2007-04-14 |
wenzelm |
2007-04-14 |
tuned signature;
export: precomputed closure, no reference to contexts;
|
file | diff | annotate |
| 2007-04-04 |
wenzelm |
2007-04-04 |
renamed Variable.importT to importT_thms;
|
file | diff | annotate |
| 2007-04-03 |
wenzelm |
2007-04-03 |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file | diff | annotate |
| 2006-12-12 |
wenzelm |
2006-12-12 |
tuned expand_binds;
|
file | diff | annotate |
| 2006-12-06 |
wenzelm |
2006-12-06 |
moved hidden_polymorphism to term.ML;
|
file | diff | annotate |
| 2006-11-28 |
wenzelm |
2006-11-28 |
added add_fixed;
|
file | diff | annotate |
| 2006-11-24 |
wenzelm |
2006-11-24 |
added export_morphism;
ProofContext.init;
|
file | diff | annotate |
| 2006-11-14 |
wenzelm |
2006-11-14 |
removed fix_frees interface;
added auto_fixes (depends on body mode);
|
file | diff | annotate |
| 2006-11-14 |
wenzelm |
2006-11-14 |
declare_constraints: reset constraint on dummyS;
|
file | diff | annotate |
| 2006-11-10 |
wenzelm |
2006-11-10 |
tuned Variable.trade;
|
file | diff | annotate |
| 2006-09-30 |
wenzelm |
2006-09-30 |
renamed Variable.invent_fixes to Variable.variant_fixes;
|
file | diff | annotate |