2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
2009-07-25 |
wenzelm |
renamed structure Display_Goal to Goal_Display;
|
file |
diff |
annotate
|
2009-07-23 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
file |
diff |
annotate
|
2009-07-20 |
wenzelm |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
|
file |
diff |
annotate
|
2009-07-17 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
2009-07-16 |
wenzelm |
incr_indexes (from Proofterm);
|
file |
diff |
annotate
|
2009-07-06 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
2009-07-02 |
wenzelm |
added pro-forma proof constructor Inclass;
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
2009-03-01 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
2009-02-27 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
2009-01-26 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
file |
diff |
annotate
|
2008-12-31 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
2008-12-30 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
2008-12-30 |
wenzelm |
canonical Term.add_var_names, Term.add_tvar_namesT;
|
file |
diff |
annotate
|
2008-11-16 |
berghofe |
- Corrected order of quantification over Frees.
|
file |
diff |
annotate
|
2008-11-15 |
wenzelm |
adapted PThm;
|
file |
diff |
annotate
|
2008-06-23 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
2008-05-18 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
2008-03-19 |
haftmann |
Type.lookup now curried
|
file |
diff |
annotate
|
2007-10-30 |
berghofe |
Handle Subscript exception when looking up bound variables.
|
file |
diff |
annotate
|
2007-05-31 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
2006-12-04 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
2006-10-31 |
haftmann |
fixed type signature of Type.varify
|
file |
diff |
annotate
|
2006-09-21 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
2006-09-15 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
2006-08-02 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2006-06-11 |
wenzelm |
avoid unqualified exception;
|
file |
diff |
annotate
|
2006-04-27 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
2006-04-26 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2006-04-13 |
wenzelm |
ignore sorts of consts declarations;
|
file |
diff |
annotate
|
2006-03-21 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
2006-02-06 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
2005-11-16 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
2005-09-15 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
2005-09-02 |
haftmann |
some 'assoc' etc. refactoring
|
file |
diff |
annotate
|
2005-09-01 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
2005-08-01 |
wenzelm |
replaced atless by term_ord;
|
file |
diff |
annotate
|
2005-07-28 |
wenzelm |
Sign.typ_unify;
|
file |
diff |
annotate
|
2005-07-19 |
wenzelm |
Logic.incr_tvar;
|
file |
diff |
annotate
|
2005-07-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-07-13 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
2005-04-21 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
2005-03-04 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
2005-03-03 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
2005-02-13 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
2004-06-21 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
2004-06-05 |
wenzelm |
pretty_thm/goals_aux, pretty_flexpair: pp;
|
file |
diff |
annotate
|
2004-06-01 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
2002-11-27 |
berghofe |
prop_of now returns proposition in beta-eta normal form.
|
file |
diff |
annotate
|
2002-11-13 |
berghofe |
Improved function decompose.
|
file |
diff |
annotate
|
2002-10-21 |
berghofe |
- reconstruct_proof no longer relies on TypeInfer.infer_types
|
file |
diff |
annotate
|
2002-09-30 |
berghofe |
Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
|
file |
diff |
annotate
|
2002-07-10 |
berghofe |
expand_proof now also takes an optional term describing the proposition
|
file |
diff |
annotate
|
2002-06-28 |
berghofe |
Added function prop_of' taking assumption context as an argument.
|
file |
diff |
annotate
|
2002-05-11 |
berghofe |
- Tuned function mk_cnstrts
|
file |
diff |
annotate
|
2002-02-06 |
berghofe |
Indexes of variables in expanded proofs are now incremented to avoid clashes.
|
file |
diff |
annotate
|
2001-12-18 |
wenzelm |
tuned Type.unify;
|
file |
diff |
annotate
|
2001-11-19 |
berghofe |
Moved fastype to Envir.
|
file |
diff |
annotate
|