| 2008-03-19 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| 2008-03-19 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| 2007-10-11 |
wenzelm |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
file |
diff |
annotate
|
| 2007-09-25 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| 2007-09-25 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| 2007-09-18 |
wenzelm |
simplified PrintMode interfaces;
|
file |
diff |
annotate
|
| 2007-09-18 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| 2007-04-15 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
| 2007-04-15 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| 2007-04-04 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| 2006-10-04 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| 2006-09-06 |
haftmann |
TypedefPackage.add_typedef_* now yields name of introduced type constructor
|
file |
diff |
annotate
|
| 2006-08-02 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
| 2006-07-04 |
wenzelm |
Thm.varifyT;
|
file |
diff |
annotate
|
| 2006-06-13 |
wenzelm |
use Drule.unvarify instead of obsolete Drule.freeze_all;
|
file |
diff |
annotate
|
| 2006-05-20 |
wenzelm |
List.partition;
|
file |
diff |
annotate
|
| 2006-04-06 |
haftmann |
cleanup in typedef/datatype package
|
file |
diff |
annotate
|
| 2006-03-14 |
wenzelm |
string_of_mixfix;
|
file |
diff |
annotate
|
| 2006-02-16 |
obua |
cache improvements
|
file |
diff |
annotate
|
| 2006-02-16 |
obua |
variable counter is now also cached
|
file |
diff |
annotate
|
| 2006-02-16 |
obua |
adapted to kernel changes
|
file |
diff |
annotate
|
| 2006-02-15 |
obua |
fixed bugs, added caching
|
file |
diff |
annotate
|
| 2006-02-06 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| 2006-01-21 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| 2006-01-14 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| 2005-12-22 |
paulson |
Fixed a use of an outdated Substring function
|
file |
diff |
annotate
|
| 2005-12-06 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| 2005-10-21 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| 2005-10-19 |
wenzelm |
replaced commafy by existing commas;
|
file |
diff |
annotate
|
| 2005-10-18 |
wenzelm |
Simplifier.theory_context;
|
file |
diff |
annotate
|
| 2005-09-26 |
wenzelm |
moved disambiguate_frees to ProofKernel;
|
file |
diff |
annotate
|
| 2005-09-26 |
obua |
Release HOL4 and HOLLight Importer.
|
file |
diff |
annotate
|
| 2005-09-26 |
obua |
fixed disambiguation problem
|
file |
diff |
annotate
|
| 2005-09-24 |
obua |
set show_types and show_sorts during import
|
file |
diff |
annotate
|
| 2005-09-24 |
obua |
remove debug clutter
|
file |
diff |
annotate
|
| 2005-09-24 |
obua |
bug fix
|
file |
diff |
annotate
|
| 2005-09-23 |
obua |
fix
|
file |
diff |
annotate
|
| 2005-09-23 |
obua |
1) fixed bug in type_introduction: first stage uses different namespace than second stage
|
file |
diff |
annotate
|
| 2005-09-23 |
obua |
replay type_introduction fix
|
file |
diff |
annotate
|
| 2005-09-22 |
obua |
add debug messages
|
file |
diff |
annotate
|
| 2005-09-19 |
obua |
maybe the last bug fix (sigh)?
|
file |
diff |
annotate
|
| 2005-09-17 |
obua |
1) mapped .. and == constants
|
file |
diff |
annotate
|
| 2005-09-16 |
obua |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
file |
diff |
annotate
|
| 2005-09-15 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| 2005-09-14 |
obua |
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
|
file |
diff |
annotate
|
| 2005-09-13 |
obua |
fixed INST: has same semantic now as INST_TYPE for repetitions
|
file |
diff |
annotate
|
| 2005-09-12 |
obua |
removed clutter
|
file |
diff |
annotate
|
| 2005-09-12 |
obua |
introduced internal function hthm2thm
|
file |
diff |
annotate
|
| 2005-09-12 |
obua |
Added HOLLight support to importer.
|
file |
diff |
annotate
|
| 2005-06-20 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
| 2005-06-17 |
wenzelm |
refer to HOL4_PROOFS setting;
|
file |
diff |
annotate
|
| 2005-06-11 |
wenzelm |
renamed Sign.intern_tycon to Sign.intern_type;
|
file |
diff |
annotate
|
| 2005-04-21 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
| 2005-04-01 |
skalberg |
Updated import configuration.
|
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
|
| 2005-01-24 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| 2004-06-20 |
wenzelm |
got rid of Output.output for default print mode;
|
file |
diff |
annotate
|