| 1997-11-04 |
oheimb |
1997-11-04 |
* removed "axioms" and "generated by" section
* replaced "ops" section by extended "consts" section, which is capable of
handling the continuous function space "->" directly
* domain package: now uses normal mixfix annotations (instead of cinfix...)
|
file | diff | annotate |
| 1997-10-30 |
oheimb |
1997-10-30 |
domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
|
file | diff | annotate |
| 1997-10-27 |
wenzelm |
1997-10-27 |
do not change global_names flag;
|
file | diff | annotate |
| 1997-10-27 |
oheimb |
1997-10-27 |
adapted domain and ax_ops package for name spaces
|
file | diff | annotate |
| 1997-10-20 |
wenzelm |
1997-10-20 |
set global_names;
|
file | diff | annotate |
| 1997-08-06 |
wenzelm |
1997-08-06 |
tuned;
removed qed_spec_mp;
|
file | diff | annotate |
| 1997-08-06 |
berghofe |
1997-08-06 |
Replaced "init_thy_reader" by set_parser.
|
file | diff | annotate |
| 1997-07-09 |
wenzelm |
1997-07-09 |
removed obsolete init_pps and init_thy_reader;
|
file | diff | annotate |
| 1996-12-13 |
oheimb |
1996-12-13 |
adaptions for symbol font
|
file | diff | annotate |
| 1996-12-09 |
sandnerr |
1996-12-09 |
qed_spec_mp moved to end of file
|
file | diff | annotate |
| 1996-11-29 |
wenzelm |
1996-11-29 |
added qed_spec_mp (from HOL);
|
file | diff | annotate |
| 1996-11-29 |
oheimb |
1996-11-29 |
*** empty log message ***
|
file | diff | annotate |
| 1996-11-29 |
oheimb |
1996-11-29 |
renamed is_flat to flat,
moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
(*lift* to *up*, except Ilift to Ifup, lift to fup)
|
file | diff | annotate |
| 1996-09-26 |
paulson |
1996-09-26 |
Ran expandshort; used stac instead of ssubst
|
file | diff | annotate |
| 1996-05-31 |
oheimb |
1996-05-31 |
introduced forgotten bind_thm calls
|
file | diff | annotate |
| 1996-03-12 |
regensbu |
1996-03-12 |
added ' make_html:=false;' to end of ROOT file
|
file | diff | annotate |
| 1996-01-30 |
clasohm |
1996-01-30 |
expanded tabs
|
file | diff | annotate |
| 1995-11-21 |
clasohm |
1995-11-21 |
main directory is now read by exit_use_dir, too;
removed make_chart from ROOT.ML
|
file | diff | annotate |
| 1995-10-25 |
clasohm |
1995-10-25 |
added init_html and make_chart
|
file | diff | annotate |
| 1995-10-17 |
regensbu |
1995-10-17 |
removed incompatibility with sml
|
file | diff | annotate |
| 1995-10-06 |
regensbu |
1995-10-06 |
added 8bit pragmas
added directory ax_ops for sections axioms and ops
added directory domain for sections domain and generated
this is the type definition package of David Oheimb
|
file | diff | annotate |
| 1995-10-04 |
clasohm |
1995-10-04 |
added local simpsets
|
file | diff | annotate |
| 1995-06-29 |
regensbu |
1995-06-29 |
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
|
file | diff | annotate |
| 1995-03-17 |
regensbu |
1995-03-17 |
Removed bugs which occurred due to new generation mechanism for type variables
|
file | diff | annotate |
| 1994-10-06 |
nipkow |
1994-10-06 |
New version
|
file | diff | annotate |
| 1994-05-19 |
wenzelm |
1994-05-19 |
thy reader now initialised by init_thy_reader();
|
file | diff | annotate |
| 1994-03-24 |
nipkow |
1994-03-24 |
Franz fragen
|
file | diff | annotate |
| 1994-01-19 |
nipkow |
1994-01-19 |
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
|
file | diff | annotate |