Thu, 24 Aug 2000 00:53:23 +0200 |
wenzelm |
choosefrom: easy settings;
|
changeset |
files
|
Wed, 23 Aug 2000 15:24:46 +0200 |
wenzelm |
isabelle env: trivlist;
|
changeset |
files
|
Tue, 22 Aug 2000 11:24:44 +0200 |
paulson |
removed redundant commands
|
changeset |
files
|
Tue, 22 Aug 2000 11:24:24 +0200 |
paulson |
removed most "makeatother", no longer needed
|
changeset |
files
|
Tue, 22 Aug 2000 10:59:15 +0200 |
paulson |
updated to latest versions of ttbox and ttbreak
|
changeset |
files
|
Mon, 21 Aug 2000 19:29:27 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 21 Aug 2000 19:17:07 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 21 Aug 2000 19:03:58 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 21 Aug 2000 18:49:38 +0200 |
wenzelm |
tuned translations;
|
changeset |
files
|
Mon, 21 Aug 2000 18:45:29 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Mon, 21 Aug 2000 18:40:30 +0200 |
wenzelm |
added \isastyleminor;
|
changeset |
files
|
Mon, 21 Aug 2000 18:38:27 +0200 |
wenzelm |
more \isachars;
|
changeset |
files
|
Mon, 21 Aug 2000 18:16:47 +0200 |
wenzelm |
fixed has_meta_prems: strip_assums_hyp;
|
changeset |
files
|
Mon, 21 Aug 2000 17:54:43 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Mon, 21 Aug 2000 13:47:24 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Sun, 20 Aug 2000 17:45:20 +0200 |
wenzelm |
open cases;
|
changeset |
files
|
Sat, 19 Aug 2000 12:49:19 +0200 |
wenzelm |
output \isachar;
|
changeset |
files
|
Sat, 19 Aug 2000 12:48:26 +0200 |
wenzelm |
cond_add_path;
|
changeset |
files
|
Sat, 19 Aug 2000 12:47:16 +0200 |
wenzelm |
fixed text;
|
changeset |
files
|
Sat, 19 Aug 2000 12:45:11 +0200 |
wenzelm |
turned into new-style theory;
|
changeset |
files
|
Sat, 19 Aug 2000 12:44:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 19 Aug 2000 12:44:20 +0200 |
wenzelm |
tuned \isastyle;
|
changeset |
files
|
Sat, 19 Aug 2000 12:43:55 +0200 |
wenzelm |
added \isachar definitions;
|
changeset |
files
|
Sat, 19 Aug 2000 12:42:52 +0200 |
wenzelm |
%\urlstyle{rm}
|
changeset |
files
|
Sat, 19 Aug 2000 12:41:41 +0200 |
wenzelm |
renamed cond_with_path to cond_add_path (add to front);
|
changeset |
files
|
Fri, 18 Aug 2000 18:46:02 +0200 |
paulson |
X-symbols for ordinal, cardinal, integer arithmetic
|
changeset |
files
|
Fri, 18 Aug 2000 18:11:10 +0200 |
wenzelm |
fixed RuleCases.make (invert flag);
|
changeset |
files
|
Fri, 18 Aug 2000 18:06:10 +0200 |
wenzelm |
removed obsolete add_recdef_x;
|
changeset |
files
|
Fri, 18 Aug 2000 17:58:33 +0200 |
wenzelm |
proper handling of defs;
|
changeset |
files
|
Fri, 18 Aug 2000 17:53:49 +0200 |
wenzelm |
Main now new-style theory; added Main.ML for compatibility;
|
changeset |
files
|
Fri, 18 Aug 2000 12:34:48 +0200 |
paulson |
simproc bug fix: only TYPING assumptions are given to the simplifier
|
changeset |
files
|
Fri, 18 Aug 2000 12:34:13 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
Fri, 18 Aug 2000 12:31:20 +0200 |
paulson |
new example ZF/ex/NatSum
|
changeset |
files
|
Fri, 18 Aug 2000 12:30:41 +0200 |
paulson |
now allows dest_coeff to fail
|
changeset |
files
|
Fri, 18 Aug 2000 11:14:23 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Fri, 18 Aug 2000 10:34:08 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Thu, 17 Aug 2000 21:07:25 +0200 |
wenzelm |
removed obsolete keyword;
|
changeset |
files
|
Thu, 17 Aug 2000 21:06:04 +0200 |
wenzelm |
fixed indexing;
|
changeset |
files
|
Thu, 17 Aug 2000 18:58:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 17 Aug 2000 18:31:12 +0200 |
nipkow |
installed recdef congs data
|
changeset |
files
|
Thu, 17 Aug 2000 18:30:48 +0200 |
nipkow |
added map_cong to recdef
|
changeset |
files
|
Thu, 17 Aug 2000 16:23:50 +0200 |
wenzelm |
removed Lambda/Type.ML;
|
changeset |
files
|
Thu, 17 Aug 2000 12:02:01 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
Thu, 17 Aug 2000 12:01:09 +0200 |
paulson |
fixed a proof that had stopped working ???
|
changeset |
files
|
Thu, 17 Aug 2000 12:00:23 +0200 |
paulson |
tidied & updated proofs, deleting some unused ones
|
changeset |
files
|
Thu, 17 Aug 2000 11:56:47 +0200 |
paulson |
modified proofs: better rules for cancellation of common factors across comparisons
|
changeset |
files
|
Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
Thu, 17 Aug 2000 10:42:57 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Thu, 17 Aug 2000 10:40:31 +0200 |
wenzelm |
cases: opaque by default;
|
changeset |
files
|
Thu, 17 Aug 2000 10:39:44 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
Thu, 17 Aug 2000 10:39:30 +0200 |
wenzelm |
tuned error handling;
|
changeset |
files
|
Thu, 17 Aug 2000 10:39:12 +0200 |
wenzelm |
added 'symmetric' attribute;
|
changeset |
files
|
Thu, 17 Aug 2000 10:38:43 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Thu, 17 Aug 2000 10:38:20 +0200 |
wenzelm |
sel_upd proc: include 'more' pseudo-field;
|
changeset |
files
|
Thu, 17 Aug 2000 10:37:33 +0200 |
wenzelm |
renamed 'mk_cases_tac' to 'ind_cases';
|
changeset |
files
|
Thu, 17 Aug 2000 10:37:04 +0200 |
wenzelm |
changed 'opaque' option to 'open' (opaque is default);
|
changeset |
files
|
Thu, 17 Aug 2000 10:35:49 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
Thu, 17 Aug 2000 10:34:52 +0200 |
wenzelm |
converted to new-style theory;
|
changeset |
files
|
Thu, 17 Aug 2000 10:34:28 +0200 |
wenzelm |
done;
|
changeset |
files
|
Thu, 17 Aug 2000 10:34:11 +0200 |
wenzelm |
'symmetric' attribute;
|
changeset |
files
|