2000-08-28 |
wenzelm |
moved \tt things to ttbox.sty;
|
changeset |
files
|
2000-08-28 |
wenzelm |
proper setup;
|
changeset |
files
|
2000-08-28 |
wenzelm |
removed ttbox;
|
changeset |
files
|
2000-08-28 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2000-08-28 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2000-08-25 |
paulson |
added \trivlist...\endtrivlist to the "isabelle" environment
|
changeset |
files
|
2000-08-25 |
paulson |
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
|
changeset |
files
|
2000-08-24 |
paulson |
xsymbols for {| and |}
|
changeset |
files
|
2000-08-24 |
paulson |
xsymbols for leads-to and Join
|
changeset |
files
|
2000-08-24 |
paulson |
fixed strip_assums and assum_pairs, restoring them (essentially) to their
|
changeset |
files
|
2000-08-24 |
paulson |
added some xsymbols, and tidied
|
changeset |
files
|
2000-08-23 |
wenzelm |
more symbols;
|
changeset |
files
|
2000-08-23 |
wenzelm |
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
|
changeset |
files
|
2000-08-23 |
wenzelm |
choosefrom: support easy settings;
|
changeset |
files
|
2000-08-23 |
wenzelm |
choosefrom: easy settings;
|
changeset |
files
|
2000-08-23 |
wenzelm |
isabelle env: trivlist;
|
changeset |
files
|
2000-08-22 |
paulson |
removed redundant commands
|
changeset |
files
|
2000-08-22 |
paulson |
removed most "makeatother", no longer needed
|
changeset |
files
|
2000-08-22 |
paulson |
updated to latest versions of ttbox and ttbreak
|
changeset |
files
|
2000-08-21 |
wenzelm |
updated;
|
changeset |
files
|
2000-08-21 |
wenzelm |
updated;
|
changeset |
files
|
2000-08-21 |
wenzelm |
updated;
|
changeset |
files
|
2000-08-21 |
wenzelm |
tuned translations;
|
changeset |
files
|
2000-08-21 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2000-08-21 |
wenzelm |
added \isastyleminor;
|
changeset |
files
|
2000-08-21 |
wenzelm |
more \isachars;
|
changeset |
files
|
2000-08-21 |
wenzelm |
fixed has_meta_prems: strip_assums_hyp;
|
changeset |
files
|
2000-08-21 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2000-08-21 |
wenzelm |
updated;
|
changeset |
files
|
2000-08-20 |
wenzelm |
open cases;
|
changeset |
files
|
2000-08-19 |
wenzelm |
output \isachar;
|
changeset |
files
|
2000-08-19 |
wenzelm |
cond_add_path;
|
changeset |
files
|
2000-08-19 |
wenzelm |
fixed text;
|
changeset |
files
|
2000-08-19 |
wenzelm |
turned into new-style theory;
|
changeset |
files
|
2000-08-19 |
wenzelm |
tuned;
|
changeset |
files
|
2000-08-19 |
wenzelm |
tuned \isastyle;
|
changeset |
files
|
2000-08-19 |
wenzelm |
added \isachar definitions;
|
changeset |
files
|
2000-08-19 |
wenzelm |
%\urlstyle{rm}
|
changeset |
files
|
2000-08-19 |
wenzelm |
renamed cond_with_path to cond_add_path (add to front);
|
changeset |
files
|
2000-08-18 |
paulson |
X-symbols for ordinal, cardinal, integer arithmetic
|
changeset |
files
|
2000-08-18 |
wenzelm |
fixed RuleCases.make (invert flag);
|
changeset |
files
|
2000-08-18 |
wenzelm |
removed obsolete add_recdef_x;
|
changeset |
files
|
2000-08-18 |
wenzelm |
proper handling of defs;
|
changeset |
files
|
2000-08-18 |
wenzelm |
Main now new-style theory; added Main.ML for compatibility;
|
changeset |
files
|
2000-08-18 |
paulson |
simproc bug fix: only TYPING assumptions are given to the simplifier
|
changeset |
files
|
2000-08-18 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
2000-08-18 |
paulson |
new example ZF/ex/NatSum
|
changeset |
files
|
2000-08-18 |
paulson |
now allows dest_coeff to fail
|
changeset |
files
|