2000-04-13 |
wenzelm |
use HOLogic.termT;
|
file |
diff |
annotate
|
2000-03-31 |
nipkow |
comments modified
|
file |
diff |
annotate
|
2000-03-30 |
nipkow |
the simplification rules returned from TFL are now paired with the row they
|
file |
diff |
annotate
|
2000-03-20 |
paulson |
replaced best_tac by force_tac, allowing some arithmetic reasoning
|
file |
diff |
annotate
|
1999-08-18 |
paulson |
from Konrad: support for schematic definitions
|
file |
diff |
annotate
|
1999-04-30 |
wenzelm |
tuned defer_recdef interfaces;
|
file |
diff |
annotate
|
1999-04-27 |
wenzelm |
proper quiet_mode;
|
file |
diff |
annotate
|
1999-04-23 |
paulson |
Now for recdefs that omit the WF relation;
|
file |
diff |
annotate
|
1999-04-22 |
wenzelm |
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
|
file |
diff |
annotate
|
1999-04-20 |
wenzelm |
temporarily reverted to 1.24;
|
file |
diff |
annotate
|
1999-04-16 |
wenzelm |
Sign.base_name fid;
|
file |
diff |
annotate
|
1999-04-14 |
wenzelm |
quiet_mode;
|
file |
diff |
annotate
|
1999-03-17 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
1999-03-10 |
paulson |
allow meta_outer to do nothing
|
file |
diff |
annotate
|
1998-11-25 |
wenzelm |
replaced prs by writeln;
|
file |
diff |
annotate
|
1998-06-30 |
berghofe |
Removed structure Prod_Syntax.
|
file |
diff |
annotate
|
1998-05-27 |
paulson |
Changed require to requires for MLWorks
|
file |
diff |
annotate
|
1998-04-29 |
wenzelm |
Theory.require;
|
file |
diff |
annotate
|
1998-04-10 |
paulson |
can prove the empty relation to be WF
|
file |
diff |
annotate
|
1997-11-03 |
wenzelm |
CLASET';
|
file |
diff |
annotate
|
1997-10-23 |
wenzelm |
Sign.stamp_names_of;
|
file |
diff |
annotate
|
1997-10-17 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
1997-07-24 |
nipkow |
Replaced clumsy rewriting by the new function simplify on thms.
|
file |
diff |
annotate
|
1997-07-23 |
wenzelm |
tmp fix to accomodate rep_ss changes;
|
file |
diff |
annotate
|
1997-07-04 |
paulson |
Now catches the error of calling tgoalw when there are no goals to prove,
|
file |
diff |
annotate
|
1997-06-23 |
paulson |
Removal of structure Context and its replacement by a theorem list of
|
file |
diff |
annotate
|
1997-06-05 |
paulson |
Numerous simplifications and removal of HOL-isms
|
file |
diff |
annotate
|
1997-06-03 |
paulson |
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
|
file |
diff |
annotate
|
1997-05-26 |
paulson |
Now checks the name of the function being defined
|
file |
diff |
annotate
|
1997-05-22 |
paulson |
New headers and other minor changes
|
file |
diff |
annotate
|
1997-05-21 |
paulson |
Basis library input/output primitives; currying the induction rule;
|
file |
diff |
annotate
|
1997-05-20 |
paulson |
Removal of redundant code (unused or already present in Isabelle.
|
file |
diff |
annotate
|
1997-05-16 |
paulson |
Subst now moved to directory HOL
|
file |
diff |
annotate
|
1997-05-15 |
paulson |
TFL now integrated with HOL (more work needed)
|
file |
diff |
annotate
|
1997-01-03 |
paulson |
Conversion to Basis Library (using prs instead of output)
|
file |
diff |
annotate
|
1996-10-18 |
paulson |
Konrad Slind's TFL
|
file |
diff |
annotate
|