| Thu, 08 May 1997 12:22:01 +0200 |
paulson |
New proofs about WHILE and VALOF
|
changeset |
files
|
| Thu, 08 May 1997 11:44:59 +0200 |
nipkow |
Modified def of Least, which, as Markus correctly complained, looked like
|
changeset |
files
|
| Thu, 08 May 1997 10:20:37 +0200 |
paulson |
Made a slow proof slightly faster
|
changeset |
files
|
| Thu, 08 May 1997 10:19:52 +0200 |
paulson |
Changed from fast_tac to blast_tac
|
changeset |
files
|
| Wed, 07 May 1997 18:39:04 +0200 |
wenzelm |
misc minor improvements;
|
changeset |
files
|
| Wed, 07 May 1997 18:37:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 07 May 1997 18:37:12 +0200 |
wenzelm |
replaced Int by IntPr, result by qed;
|
changeset |
files
|
| Wed, 07 May 1997 18:36:13 +0200 |
wenzelm |
fixed ref to srcs;
|
changeset |
files
|
| Wed, 07 May 1997 18:35:56 +0200 |
wenzelm |
fixed caption font;
|
changeset |
files
|
| Wed, 07 May 1997 17:21:24 +0200 |
wenzelm |
tuned spaces;
|
changeset |
files
|
| Wed, 07 May 1997 17:21:04 +0200 |
wenzelm |
fixed braces;
|
changeset |
files
|
| Wed, 07 May 1997 17:16:36 +0200 |
paulson |
stylistic improvements
|
changeset |
files
|
| Wed, 07 May 1997 17:16:18 +0200 |
paulson |
Documents directory Induct; stylistic improvements
|
changeset |
files
|
| Wed, 07 May 1997 17:15:57 +0200 |
paulson |
New acknowledgements
|
changeset |
files
|
| Wed, 07 May 1997 16:40:00 +0200 |
wenzelm |
fixed witness syntax;
|
changeset |
files
|
| Wed, 07 May 1997 16:38:33 +0200 |
wenzelm |
SYNC;
|
changeset |
files
|
| Wed, 07 May 1997 16:29:06 +0200 |
paulson |
New acknowledgements; fixed overfull lines and tables
|
changeset |
files
|
| Wed, 07 May 1997 16:26:28 +0200 |
paulson |
New acknowledgements; no Fast_tac
|
changeset |
files
|
| Wed, 07 May 1997 16:26:02 +0200 |
paulson |
Larry's private LaTeX-2e version
|
changeset |
files
|
| Wed, 07 May 1997 13:51:22 +0200 |
paulson |
Moved induction examples to directory Induct
|
changeset |
files
|
| Wed, 07 May 1997 13:50:52 +0200 |
paulson |
changed title to README
|
changeset |
files
|
| Wed, 07 May 1997 13:50:18 +0200 |
paulson |
Documentation for directory "ex"
|
changeset |
files
|
| Wed, 07 May 1997 13:49:57 +0200 |
paulson |
Documentation for directory "Induct"
|
changeset |
files
|
| Wed, 07 May 1997 13:01:43 +0200 |
paulson |
Conversion to use blast_tac (with other improvements)
|
changeset |
files
|
| Wed, 07 May 1997 12:50:26 +0200 |
paulson |
New directory to contain examples of (co)inductive definitions
|
changeset |
files
|
| Wed, 07 May 1997 12:49:02 +0200 |
paulson |
Description of the Auth directory: security protocols proofs
|
changeset |
files
|
| Tue, 06 May 1997 15:27:35 +0200 |
wenzelm |
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
|
changeset |
files
|
| Tue, 06 May 1997 15:24:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 06 May 1997 15:04:53 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Tue, 06 May 1997 14:36:37 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 06 May 1997 13:49:29 +0200 |
wenzelm |
fixed simplifier ex;
|
changeset |
files
|
| Tue, 06 May 1997 13:43:54 +0200 |
wenzelm |
SYNC;
|
changeset |
files
|
| Tue, 06 May 1997 13:42:28 +0200 |
wenzelm |
fixed simplifier examples;
|
changeset |
files
|
| Tue, 06 May 1997 13:33:33 +0200 |
nipkow |
Stupid bug in induct_tac caused warning to always appear.
|
changeset |
files
|
| Tue, 06 May 1997 12:55:07 +0200 |
wenzelm |
removed MLtrans, MLtext;
|
changeset |
files
|
| Tue, 06 May 1997 12:51:23 +0200 |
wenzelm |
added \Pure, \CPure;
|
changeset |
files
|
| Tue, 06 May 1997 12:50:16 +0200 |
wenzelm |
misc updates, tuning, cleanup;
|
changeset |
files
|
| Mon, 05 May 1997 21:18:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 May 1997 18:50:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 May 1997 18:09:31 +0200 |
nipkow |
Cosmetic update of induct_tac; test first now.
|
changeset |
files
|
| Mon, 05 May 1997 13:24:38 +0200 |
wenzelm |
SYNC;
|
changeset |
files
|
| Mon, 05 May 1997 13:24:11 +0200 |
wenzelm |
misc updates, tuning, cleanup;
|
changeset |
files
|
| Mon, 05 May 1997 12:15:53 +0200 |
paulson |
Some blast_tac calls; more needed
|
changeset |
files
|
| Mon, 05 May 1997 12:15:20 +0200 |
paulson |
Again "norm" DOES NOT normalize bodies of abstractions
|
changeset |
files
|
| Fri, 02 May 1997 18:19:25 +0200 |
wenzelm |
fixed comment;
|
changeset |
files
|
| Fri, 02 May 1997 18:19:01 +0200 |
wenzelm |
-P option (prune empty dirs);
|
changeset |
files
|
| Fri, 02 May 1997 16:41:35 +0200 |
berghofe |
Updated to LaTeX 2e
|
changeset |
files
|
| Fri, 02 May 1997 16:21:04 +0200 |
berghofe |
New version of rail.sty for LaTeX 2e
|
changeset |
files
|
| Fri, 02 May 1997 16:18:49 +0200 |
berghofe |
Updated to LaTeX 2e
|
changeset |
files
|
| Fri, 02 May 1997 16:18:11 +0200 |
berghofe |
Version of the proof macros for LaTeX 2e
|
changeset |
files
|
| Fri, 02 May 1997 16:16:22 +0200 |
berghofe |
This file is now replaced by proof.sty
|
changeset |
files
|
| Fri, 02 May 1997 10:19:19 +0200 |
paulson |
Higher bound means much faster proof
|
changeset |
files
|
| Fri, 02 May 1997 10:18:50 +0200 |
paulson |
More tracing. hyp_subst_tac allowed to fail
|
changeset |
files
|
| Fri, 02 May 1997 10:17:44 +0200 |
paulson |
New blast_tac call: made possible by bug fix involving equality substitution
|
changeset |
files
|
| Thu, 01 May 1997 10:28:10 +0200 |
paulson |
No longer proves mutual_induct unless it is necessary.
|
changeset |
files
|
| Wed, 30 Apr 1997 16:36:59 +0200 |
paulson |
Documented blast_tac
|
changeset |
files
|
| Wed, 30 Apr 1997 16:36:38 +0200 |
paulson |
Automatic update
|
changeset |
files
|
| Wed, 30 Apr 1997 16:33:43 +0200 |
paulson |
Indexing for trace_simp
|
changeset |
files
|
| Wed, 30 Apr 1997 13:40:40 +0200 |
paulson |
No longer proves mutual induction rules unless they are needed
|
changeset |
files
|
| Wed, 30 Apr 1997 13:39:56 +0200 |
paulson |
Fixed clasets so that blast_tac would work
|
changeset |
files
|
| Wed, 30 Apr 1997 13:38:38 +0200 |
paulson |
Now modified for sml/nj 109.27
|
changeset |
files
|
| Wed, 30 Apr 1997 12:59:24 +0200 |
paulson |
More tracing; less exception handling
|
changeset |
files
|
| Wed, 30 Apr 1997 12:13:17 +0200 |
wenzelm |
improved the space2 glyph;
|
changeset |
files
|
| Wed, 30 Apr 1997 12:06:18 +0200 |
mueller |
added IOA (meta theory and ABP, NTP examples);
|
changeset |
files
|
| Wed, 30 Apr 1997 12:05:45 +0200 |
mueller |
fixed Id;
|
changeset |
files
|
| Wed, 30 Apr 1997 11:58:23 +0200 |
mueller |
removed (most of) IOA (see HOLCF/IOA);
|
changeset |
files
|
| Wed, 30 Apr 1997 11:56:17 +0200 |
mueller |
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
|
changeset |
files
|
| Wed, 30 Apr 1997 11:55:22 +0200 |
mueller |
moved to .. (see also new version in HOLCF/IOA/meta_theory);
|
changeset |
files
|
| Wed, 30 Apr 1997 11:53:30 +0200 |
mueller |
removed -- new version in HOLCF/IOA/NTP;
|
changeset |
files
|
| Wed, 30 Apr 1997 11:51:28 +0200 |
mueller |
remove -- new version in HOLCF/IOA/ABP;
|
changeset |
files
|
| Wed, 30 Apr 1997 11:42:37 +0200 |
paulson |
New theorems Pow_in_Vfrom and Pow_in_VLimit
|
changeset |
files
|
| Wed, 30 Apr 1997 11:25:31 +0200 |
mueller |
Old NTP files now running under the IOA meta theory based on HOLCF;
|
changeset |
files
|
| Wed, 30 Apr 1997 11:24:14 +0200 |
mueller |
Old ABP files now running under the IOA meta theory based on HOLCF;
|
changeset |
files
|
| Wed, 30 Apr 1997 11:20:15 +0200 |
mueller |
New meta theory for IOA based on HOLCF.
|
changeset |
files
|
| Wed, 30 Apr 1997 11:11:57 +0200 |
wenzelm |
improved display of non-ASCII chars;
|
changeset |
files
|
| Tue, 29 Apr 1997 17:44:26 +0200 |
wenzelm |
fixed enc_start;
|
changeset |
files
|
| Tue, 29 Apr 1997 17:38:02 +0200 |
wenzelm |
deactivated new symbols (not yet printable on xterm, emacs);
|
changeset |
files
|
| Tue, 29 Apr 1997 17:23:53 +0200 |
wenzelm |
renamed \<choice> to \<orelse>;
|
changeset |
files
|
| Tue, 29 Apr 1997 17:14:06 +0200 |
wenzelm |
added \<orelse> symbols syntax for case;
|
changeset |
files
|
| Tue, 29 Apr 1997 17:13:41 +0200 |
wenzelm |
added \<langle>, \<rangle> symbols syntax;
|
changeset |
files
|
| Tue, 29 Apr 1997 16:39:13 +0200 |
wenzelm |
added new chars;
|
changeset |
files
|
| Tue, 29 Apr 1997 16:38:16 +0200 |
wenzelm |
is_blank: added space2 (160);
|
changeset |
files
|
| Fri, 25 Apr 1997 18:11:22 +0200 |
wenzelm |
improved DVI_VIEWER default;
|
changeset |
files
|
| Fri, 25 Apr 1997 17:50:55 +0200 |
wenzelm |
improved tmp comment;
|
changeset |
files
|
| Fri, 25 Apr 1997 17:28:43 +0200 |
wenzelm |
removed -norc;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:33:19 +0200 |
slotosch |
used explcite tactics in instances (since ax_per_trans "loops")
|
changeset |
files
|
| Fri, 25 Apr 1997 15:31:51 +0200 |
slotosch |
changed Domain->Dom for SML/NJ
|
changeset |
files
|
| Fri, 25 Apr 1997 15:24:07 +0200 |
wenzelm |
removed -c option;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:18:58 +0200 |
wenzelm |
removed -c option;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:10:52 +0200 |
wenzelm |
removed COPYDB flag;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:08:52 +0200 |
wenzelm |
removed -c option;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:08:25 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 25 Apr 1997 15:06:21 +0200 |
wenzelm |
no longer forces default;
|
changeset |
files
|
| Fri, 25 Apr 1997 14:12:33 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 25 Apr 1997 11:11:52 +0200 |
oheimb |
removed one blank at end of line 37
|
changeset |
files
|
| Thu, 24 Apr 1997 19:47:53 +0200 |
wenzelm |
refer to SOME, NONE on top-level;
|
changeset |
files
|
| Thu, 24 Apr 1997 19:46:24 +0200 |
wenzelm |
adapted for 1.09.27 (and later);
|
changeset |
files
|
| Thu, 24 Apr 1997 19:46:05 +0200 |
wenzelm |
open General (type option is in Option in the newer versions, but always
|
changeset |
files
|
| Thu, 24 Apr 1997 19:41:00 +0200 |
wenzelm |
adapted to SML/NJ 1.09.27;
|
changeset |
files
|
| Thu, 24 Apr 1997 19:08:32 +0200 |
nipkow |
Added 'induct_tac'
|
changeset |
files
|
| Thu, 24 Apr 1997 18:51:14 +0200 |
nipkow |
Updates because nat_ind_tac no longer appends "1" to the ind.var.
|
changeset |
files
|
| Thu, 24 Apr 1997 18:44:32 +0200 |
wenzelm |
removed space;
|
changeset |
files
|
| Thu, 24 Apr 1997 18:38:30 +0200 |
nipkow |
induct_tac
|
changeset |
files
|
| Thu, 24 Apr 1997 18:07:35 +0200 |
mueller |
expandshort
|
changeset |
files
|
| Thu, 24 Apr 1997 18:06:46 +0200 |
nipkow |
Introduced a generic "induct_tac" which picks up the right induction scheme
|
changeset |
files
|
| Thu, 24 Apr 1997 18:03:23 +0200 |
nipkow |
get_thydata accesses the second component of the data field. This component
|
changeset |
files
|
| Thu, 24 Apr 1997 18:00:22 +0200 |
mueller |
Main changes are:
|
changeset |
files
|
| Thu, 24 Apr 1997 17:59:55 +0200 |
nipkow |
rename_params_rule used to check if the new name clashed with a free name in
|
changeset |
files
|
| Thu, 24 Apr 1997 17:51:27 +0200 |
mueller |
deleted definitions for blift and plift
|
changeset |
files
|
| Thu, 24 Apr 1997 17:50:34 +0200 |
mueller |
Complete Redesign of Theory, main points are:
|
changeset |
files
|
| Thu, 24 Apr 1997 17:40:30 +0200 |
mueller |
added liftpair definition
|
changeset |
files
|
| Thu, 24 Apr 1997 17:38:33 +0200 |
mueller |
only in comments
|
changeset |
files
|
| Thu, 24 Apr 1997 17:35:47 +0200 |
mueller |
minor changes due to more powerful continuity check in Lift3.ML
|
changeset |
files
|
| Thu, 24 Apr 1997 17:04:07 +0200 |
mueller |
added some comments;
|
changeset |
files
|
| Thu, 24 Apr 1997 11:21:46 +0200 |
paulson |
Addition of printed tracing. Also some tidying
|
changeset |
files
|
| Thu, 24 Apr 1997 11:20:56 +0200 |
paulson |
A bit of tidying
|
changeset |
files
|
| Thu, 24 Apr 1997 10:40:01 +0200 |
oheimb |
added dependencies on ax_ops/*.ML and domain/*.ML
|
changeset |
files
|
| Thu, 24 Apr 1997 10:39:00 +0200 |
oheimb |
changed priority of '%': now no parenteses needed for '[...] == %x. [...]'
|
changeset |
files
|
| Thu, 24 Apr 1997 09:34:59 +0200 |
slotosch |
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
|
changeset |
files
|
| Wed, 23 Apr 1997 13:23:05 +0200 |
nipkow |
Added NatDef
|
changeset |
files
|
| Wed, 23 Apr 1997 11:20:18 +0200 |
paulson |
Necessary inclusion of depth bound into blast_tac call
|
changeset |
files
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Wed, 23 Apr 1997 11:12:10 +0200 |
paulson |
Unfortunately, the \\< syntax does not always accept the beginning of a line
|
changeset |
files
|
| Wed, 23 Apr 1997 11:11:38 +0200 |
paulson |
Loop detection: before expanding a haz formula, see whether it is a duplicate
|
changeset |
files
|
| Wed, 23 Apr 1997 11:05:52 +0200 |
paulson |
Made a proof search more deterministic
|
changeset |
files
|
| Wed, 23 Apr 1997 11:05:18 +0200 |
paulson |
Improved indentation of #34
|
changeset |
files
|
| Wed, 23 Apr 1997 11:02:19 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Wed, 23 Apr 1997 11:00:48 +0200 |
paulson |
Fixed typos in comment
|
changeset |
files
|
| Wed, 23 Apr 1997 10:54:22 +0200 |
paulson |
Conversion to use blast_tac
|
changeset |
files
|
| Wed, 23 Apr 1997 10:52:49 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Wed, 23 Apr 1997 10:49:01 +0200 |
paulson |
Moved diamond_trancl (which is independent of the rest) to the top
|
changeset |
files
|
| Wed, 23 Apr 1997 10:47:36 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Wed, 23 Apr 1997 10:08:51 +0200 |
wenzelm |
simprocs called with eta contracted subterm;
|
changeset |
files
|
| Wed, 23 Apr 1997 09:14:56 +0200 |
nipkow |
Tidied up.
|
changeset |
files
|
| Tue, 22 Apr 1997 18:05:42 +0200 |
wenzelm |
fixed bash-2.0 problem;
|
changeset |
files
|
| Tue, 22 Apr 1997 11:49:55 +0200 |
wenzelm |
improved fontserver example;
|
changeset |
files
|
| Tue, 22 Apr 1997 11:45:22 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Tue, 22 Apr 1997 11:37:12 +0200 |
wenzelm |
removed -norc;
|
changeset |
files
|
| Tue, 22 Apr 1997 11:25:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Apr 1997 13:49:40 +0200 |
nipkow |
Modified credits.
|
changeset |
files
|
| Mon, 21 Apr 1997 12:16:29 +0200 |
paulson |
New elimination rule for "unique existence"
|
changeset |
files
|
| Mon, 21 Apr 1997 12:16:04 +0200 |
paulson |
New introduction rule for "unique existence"
|
changeset |
files
|
| Mon, 21 Apr 1997 11:19:28 +0200 |
paulson |
Reorganized under headings. Also documented Blast_tac and LFilter
|
changeset |
files
|
| Mon, 21 Apr 1997 10:38:46 +0200 |
paulson |
Tidied up the indentation
|
changeset |
files
|
| Mon, 21 Apr 1997 10:16:41 +0200 |
paulson |
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
|
changeset |
files
|
| Mon, 21 Apr 1997 10:16:01 +0200 |
paulson |
Penalty for branching instantiations reduced from log3 to log4.
|
changeset |
files
|
| Mon, 21 Apr 1997 10:15:00 +0200 |
paulson |
New blast_tac demo
|
changeset |
files
|
| Mon, 21 Apr 1997 10:14:31 +0200 |
paulson |
Without the type constraint, the inner equality was NOT a biconditional...
|
changeset |
files
|
| Mon, 21 Apr 1997 10:13:47 +0200 |
paulson |
Now faster without calling Blast.depth_tac
|
changeset |
files
|
| Mon, 21 Apr 1997 10:12:40 +0200 |
paulson |
Disabled the attempts for mutual induction to work so that single induction
|
changeset |
files
|
| Fri, 18 Apr 1997 17:33:26 +0200 |
nipkow |
Tuple patterns are allowed now in `case'
|
changeset |
files
|
| Fri, 18 Apr 1997 16:54:52 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 18 Apr 1997 12:01:12 +0200 |
wenzelm |
print_goals: fixed show_sorts semantics;
|
changeset |
files
|
| Fri, 18 Apr 1997 11:58:38 +0200 |
wenzelm |
tuned check_has_sort;
|
changeset |
files
|
| Fri, 18 Apr 1997 11:57:51 +0200 |
wenzelm |
removed least_sort;
|
changeset |
files
|
| Fri, 18 Apr 1997 11:55:14 +0200 |
wenzelm |
tuned err msg;
|
changeset |
files
|
| Fri, 18 Apr 1997 11:54:54 +0200 |
paulson |
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
|
changeset |
files
|
| Fri, 18 Apr 1997 11:53:55 +0200 |
paulson |
Now loads theory LList indirectly: via LFilter
|
changeset |
files
|
| Fri, 18 Apr 1997 11:53:16 +0200 |
paulson |
Now uses some "case" syntax (but could use more)
|
changeset |
files
|
| Fri, 18 Apr 1997 11:52:44 +0200 |
paulson |
New monotonicity theorems
|
changeset |
files
|
| Fri, 18 Apr 1997 11:52:19 +0200 |
paulson |
New theory: a corecursive filter functional
|
changeset |
files
|
| Fri, 18 Apr 1997 11:48:16 +0200 |
paulson |
Removed needless parentheses from translation
|
changeset |
files
|
| Fri, 18 Apr 1997 11:47:36 +0200 |
paulson |
ex/LFilter is a new theory (and dependency)
|
changeset |
files
|
| Fri, 18 Apr 1997 11:47:11 +0200 |
paulson |
Automatic update
|
changeset |
files
|
| Thu, 17 Apr 1997 19:05:01 +0200 |
wenzelm |
tuned error msgs;
|
changeset |
files
|
| Thu, 17 Apr 1997 18:46:58 +0200 |
wenzelm |
improved type check error messages;
|
changeset |
files
|
| Thu, 17 Apr 1997 18:45:43 +0200 |
wenzelm |
renamed set_ap to setmp;
|
changeset |
files
|
| Thu, 17 Apr 1997 18:17:23 +0200 |
paulson |
Automatic updates
|
changeset |
files
|
| Thu, 17 Apr 1997 18:16:12 +0200 |
paulson |
Removed the \date{} command in order to put the date of typesetting on the
|
changeset |
files
|
| Thu, 17 Apr 1997 18:10:49 +0200 |
paulson |
Corrected the informal description of coinductive definition
|
changeset |
files
|
| Thu, 17 Apr 1997 18:10:12 +0200 |
paulson |
Corrected the informal description of coinductive definition in sections 1
|
changeset |
files
|
| Thu, 17 Apr 1997 17:54:21 +0200 |
nipkow |
Added ability to have case expressions involving tuples. (via translation)
|
changeset |
files
|
| Thu, 17 Apr 1997 14:41:56 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 17 Apr 1997 14:41:26 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 17 Apr 1997 14:41:08 +0200 |
wenzelm |
added fixencoding note;
|
changeset |
files
|
| Thu, 17 Apr 1997 10:40:26 +0200 |
wenzelm |
fixed ISAMODE_HOME;
|
changeset |
files
|
| Thu, 17 Apr 1997 10:30:57 +0200 |
wenzelm |
eliminated PLATFORM;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:53:36 +0200 |
wenzelm |
removed lceil, rceil, lfloor, rfloor;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:51:03 +0200 |
wenzelm |
fixed perl path (for sunbroys);
|
changeset |
files
|
| Wed, 16 Apr 1997 18:46:01 +0200 |
wenzelm |
improved translations for subset symbols syntax: constraints;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:25:46 +0200 |
wenzelm |
moved classes / sorts to sorts.ML;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:23:25 +0200 |
wenzelm |
renamed subclass to classrel;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:22:10 +0200 |
wenzelm |
Sorts.str_of_sort;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:21:00 +0200 |
wenzelm |
Sorts.str_of_arity;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:17:38 +0200 |
wenzelm |
added sorts.ML, type_infer.ML;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:16:45 +0200 |
wenzelm |
tuned type of eq_ix, mem_ix;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:16:02 +0200 |
wenzelm |
improved inc, dec;
|
changeset |
files
|
| Wed, 16 Apr 1997 18:15:32 +0200 |
wenzelm |
Type inference (isolated from type.ML, completely reimplemented).
|
changeset |
files
|
| Wed, 16 Apr 1997 18:14:43 +0200 |
wenzelm |
Type classes and sorts (isolated from type.ML).
|
changeset |
files
|
| Wed, 16 Apr 1997 18:13:12 +0200 |
wenzelm |
improved;
|
changeset |
files
|
| Tue, 15 Apr 1997 10:23:38 +0200 |
paulson |
Partially converted to call blast_tac
|
changeset |
files
|
| Tue, 15 Apr 1997 10:23:17 +0200 |
paulson |
Addition of blast_tac benchmark
|
changeset |
files
|
| Tue, 15 Apr 1997 10:22:50 +0200 |
paulson |
Changed penalty from log2 to log3
|
changeset |
files
|
| Tue, 15 Apr 1997 10:19:14 +0200 |
paulson |
An extra call to blast_tac (illustrating a need for type instantiation)
|
changeset |
files
|
| Tue, 15 Apr 1997 10:18:01 +0200 |
paulson |
Now puts basic rewrites for lappend & lmap into the simpset
|
changeset |
files
|
| Tue, 15 Apr 1997 10:17:15 +0200 |
paulson |
Removed "AddSDs [Scons_inject];" because
|
changeset |
files
|
| Tue, 15 Apr 1997 10:15:09 +0200 |
paulson |
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
|
changeset |
files
|
| Mon, 14 Apr 1997 10:28:21 +0200 |
wenzelm |
no longer includes ~/.emacs;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:16:25 +0200 |
wenzelm |
fixed file name;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:15:07 +0200 |
wenzelm |
GENERATED TEXT;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:12:37 +0200 |
wenzelm |
tuned format;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:11:32 +0200 |
wenzelm |
GENERATED TEXT;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:10:54 +0200 |
wenzelm |
GENERATED TEXT;
|
changeset |
files
|
| Sun, 13 Apr 1997 19:10:27 +0200 |
wenzelm |
fixencoding - fix references to isabelle font encoding;
|
changeset |
files
|
| Sat, 12 Apr 1997 20:02:06 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 12 Apr 1997 20:01:38 +0200 |
wenzelm |
misc improvement;
|
changeset |
files
|
| Sat, 12 Apr 1997 20:00:11 +0200 |
wenzelm |
Setup GNU Emacs for Isabelle environment.
|
changeset |
files
|
| Sat, 12 Apr 1997 19:59:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 11 Apr 1997 17:30:15 +0200 |
wenzelm |
fixed { ... } shell syntax to accomodate bash 2.x;
|
changeset |
files
|
| Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
changeset |
files
|
| Fri, 11 Apr 1997 11:33:51 +0200 |
wenzelm |
tuned error msg;
|
changeset |
files
|
| Thu, 10 Apr 1997 18:07:27 +0200 |
paulson |
Updated discussion and references for inductive definitions
|
changeset |
files
|
| Thu, 10 Apr 1997 14:26:01 +0200 |
nipkow |
Deleted stupid proof at the end not needed anywhere.
|
changeset |
files
|
| Thu, 10 Apr 1997 12:21:21 +0200 |
nipkow |
Mod because of "Turned Addsimps into AddIffs for datatype laws."
|
changeset |
files
|
| Thu, 10 Apr 1997 12:20:55 +0200 |
nipkow |
Turned Addsimps into AddIffs for datatype laws.
|
changeset |
files
|
| Thu, 10 Apr 1997 10:55:37 +0200 |
paulson |
Changed some fast_tac to blast_tac
|
changeset |
files
|
| Thu, 10 Apr 1997 09:08:05 +0200 |
nipkow |
Added trace output and replaced fast_tac set_cs by Fast_tac.
|
changeset |
files
|
| Wed, 09 Apr 1997 15:56:53 +0200 |
oheimb |
replaced 'addwrapper' and 'addWrapper' by correct 'compwrapper' and 'compWrapper'
|
changeset |
files
|
| Wed, 09 Apr 1997 15:26:32 +0200 |
nipkow |
Thorough update.
|
changeset |
files
|
| Wed, 09 Apr 1997 12:37:44 +0200 |
paulson |
Using Blast_tac
|
changeset |
files
|
| Wed, 09 Apr 1997 12:36:52 +0200 |
paulson |
Control over excessive branching by applying a log2 penalty
|
changeset |
files
|
| Wed, 09 Apr 1997 12:34:28 +0200 |
paulson |
Explicit depth bounds seem necessary
|
changeset |
files
|
| Wed, 09 Apr 1997 12:32:04 +0200 |
paulson |
Using Blast_tac
|
changeset |
files
|
| Wed, 09 Apr 1997 12:31:11 +0200 |
paulson |
Dependency on Provers/nat_transitive
|
changeset |
files
|
| Tue, 08 Apr 1997 12:03:59 +0200 |
nipkow |
Couldn't solve n < n+1 because of missing -1
|
changeset |
files
|
| Tue, 08 Apr 1997 10:48:42 +0200 |
nipkow |
Dep. on Provers/nat_transitive
|
changeset |
files
|
| Mon, 07 Apr 1997 14:53:08 +0200 |
wenzelm |
added -t (run tests) option;
|
changeset |
files
|
| Fri, 04 Apr 1997 19:11:19 +0200 |
wenzelm |
added -g, -h options;
|
changeset |
files
|
| Fri, 04 Apr 1997 19:10:22 +0200 |
wenzelm |
tuned xdvi invocation;
|
changeset |
files
|
| Fri, 04 Apr 1997 19:09:21 +0200 |
wenzelm |
replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
|
changeset |
files
|
| Fri, 04 Apr 1997 19:08:35 +0200 |
wenzelm |
improved messages;
|
changeset |
files
|
| Fri, 04 Apr 1997 19:07:54 +0200 |
wenzelm |
fixed diagnostic output of print modes;
|
changeset |
files
|
| Fri, 04 Apr 1997 16:33:28 +0200 |
nipkow |
moved inj and surj from Set to Fun and Inv -> inv.
|
changeset |
files
|
| Fri, 04 Apr 1997 16:27:39 +0200 |
nipkow |
Inv -> inv
|
changeset |
files
|
| Fri, 04 Apr 1997 16:16:35 +0200 |
slotosch |
*** empty log message ***
|
changeset |
files
|
| Fri, 04 Apr 1997 16:04:28 +0200 |
slotosch |
Added Example Quot
|
changeset |
files
|
| Fri, 04 Apr 1997 16:03:48 +0200 |
slotosch |
Start Example
|
changeset |
files
|
| Fri, 04 Apr 1997 16:03:44 +0200 |
nipkow |
inv -> inverse
|
changeset |
files
|
| Fri, 04 Apr 1997 16:03:11 +0200 |
slotosch |
Example for higher order quotients: Fractionals
|
changeset |
files
|
| Fri, 04 Apr 1997 16:02:12 +0200 |
slotosch |
(higher-order) quotient constructor quot, based on PER
|
changeset |
files
|
| Fri, 04 Apr 1997 16:01:14 +0200 |
slotosch |
(partial) equivalecne relations. classes er<per
|
changeset |
files
|
| Fri, 04 Apr 1997 14:48:40 +0200 |
nipkow |
Inv -> inv
|
changeset |
files
|
| Fri, 04 Apr 1997 14:47:26 +0200 |
wenzelm |
added -b option (batch mode);
|
changeset |
files
|
| Fri, 04 Apr 1997 14:05:12 +0200 |
nipkow |
renamed variable 'inv'
|
changeset |
files
|
| Fri, 04 Apr 1997 14:01:18 +0200 |
wenzelm |
added Quot examples;
|
changeset |
files
|
| Fri, 04 Apr 1997 13:57:40 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Fri, 04 Apr 1997 13:56:11 +0200 |
wenzelm |
Higher-order quotients.
|
changeset |
files
|
| Fri, 04 Apr 1997 12:21:28 +0200 |
paulson |
Now calls blast_tac
|
changeset |
files
|
| Fri, 04 Apr 1997 11:33:51 +0200 |
paulson |
Another blast_tac call
|
changeset |
files
|
| Fri, 04 Apr 1997 11:32:44 +0200 |
paulson |
Simplified a proof
|
changeset |
files
|
| Fri, 04 Apr 1997 11:28:28 +0200 |
paulson |
Re-organization of the order of haz rules
|
changeset |
files
|
| Fri, 04 Apr 1997 11:27:02 +0200 |
paulson |
Calls Blast_tac. Tidied some proofs
|
changeset |
files
|
| Fri, 04 Apr 1997 11:20:31 +0200 |
paulson |
Calls Blast_tac. Tidied some proofs
|
changeset |
files
|
| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
changeset |
files
|
| Fri, 04 Apr 1997 11:18:19 +0200 |
paulson |
Adds image_eqI instead of imageI, as the former is more general
|
changeset |
files
|
| Fri, 04 Apr 1997 11:17:05 +0200 |
paulson |
Added blast.ML as a dependency
|
changeset |
files
|
| Fri, 04 Apr 1997 11:16:44 +0200 |
paulson |
Now calls Blast_tac and has some hard examples (Halting Problem
|
changeset |
files
|
| Thu, 03 Apr 1997 19:32:03 +0200 |
nipkow |
Only layout mods.
|
changeset |
files
|
| Thu, 03 Apr 1997 19:29:53 +0200 |
nipkow |
Now: unit = {True}
|
changeset |
files
|
| Thu, 03 Apr 1997 10:36:54 +0200 |
paulson |
Two extra commands shorten the proof time by 800 seconds...
|
changeset |
files
|
| Thu, 03 Apr 1997 10:33:33 +0200 |
paulson |
More List and ListPair utilities
|
changeset |
files
|
| Thu, 03 Apr 1997 10:32:34 +0200 |
paulson |
Now exports declConsts!
|
changeset |
files
|
| Thu, 03 Apr 1997 10:30:23 +0200 |
paulson |
Declares overloading for if-and-only-if
|
changeset |
files
|
| Thu, 03 Apr 1997 10:29:57 +0200 |
paulson |
Declares overloading for set-theoretic constants
|
changeset |
files
|
| Thu, 03 Apr 1997 09:46:42 +0200 |
nipkow |
Removed (Unit) in Prod.
|
changeset |
files
|
| Wed, 02 Apr 1997 19:12:26 +0200 |
wenzelm |
misc improvements;
|
changeset |
files
|
| Wed, 02 Apr 1997 17:28:27 +0200 |
wenzelm |
changed signature of dummy goal from proto_pure to pure;
|
changeset |
files
|
| Wed, 02 Apr 1997 15:39:44 +0200 |
paulson |
Converted to call blast_tac.
|
changeset |
files
|
| Wed, 02 Apr 1997 15:37:35 +0200 |
paulson |
Uses ZF.thy again, to make that theory usable
|
changeset |
files
|
| Wed, 02 Apr 1997 15:36:32 +0200 |
paulson |
Mostly converted to blast_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 15:30:44 +0200 |
paulson |
Datatype declarations now require theory Datatype--NOT in quotes
|
changeset |
files
|
| Wed, 02 Apr 1997 15:29:48 +0200 |
paulson |
Converted back from upair.thy to ZF.thy
|
changeset |
files
|
| Wed, 02 Apr 1997 15:28:42 +0200 |
paulson |
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
|
changeset |
files
|
| Wed, 02 Apr 1997 15:26:52 +0200 |
paulson |
Now checks for existence of theory Inductive (Fixedpt was too small)
|
changeset |
files
|
| Wed, 02 Apr 1997 15:25:35 +0200 |
paulson |
Now a non-trivial theory so that require_thy can find it
|
changeset |
files
|
| Wed, 02 Apr 1997 15:24:42 +0200 |
paulson |
DEEPEN now takes an upper bound for terminating searches
|
changeset |
files
|
| Wed, 02 Apr 1997 15:23:33 +0200 |
paulson |
New DEEPEN allows giving an upper bound for deepen_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 15:19:40 +0200 |
paulson |
Now builds blast_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 15:18:21 +0200 |
paulson |
Now loads blast.ML
|
changeset |
files
|
| Wed, 02 Apr 1997 15:14:37 +0200 |
paulson |
ZF.thy is again usable
|
changeset |
files
|
| Wed, 02 Apr 1997 11:59:02 +0200 |
wenzelm |
The isabelle-0 encoding table.
|
changeset |
files
|
| Wed, 02 Apr 1997 11:33:14 +0200 |
paulson |
Made the error message more explicit
|
changeset |
files
|
| Wed, 02 Apr 1997 11:32:48 +0200 |
paulson |
Now declares Basis Library version of type option
|
changeset |
files
|
| Wed, 02 Apr 1997 11:30:48 +0200 |
paulson |
Replaced Best_tac by the one rule needed for the proof
|
changeset |
files
|
| Wed, 02 Apr 1997 11:30:03 +0200 |
paulson |
Installation of blast_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 11:27:47 +0200 |
paulson |
Now tests for essential ancestors (Lfp or Gfp)
|
changeset |
files
|
| Wed, 02 Apr 1997 11:25:04 +0200 |
paulson |
Re-ordering of rules to assist blast_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 11:23:31 +0200 |
paulson |
Now loads blast_tac
|
changeset |
files
|
| Wed, 02 Apr 1997 11:19:46 +0200 |
paulson |
Reorganization of how classical rules are installed
|
changeset |
files
|
| Wed, 02 Apr 1997 11:16:40 +0200 |
paulson |
Now calls require_thy to ensure ancestors are present
|
changeset |
files
|
| Wed, 02 Apr 1997 11:15:46 +0200 |
paulson |
Implementation of blast_tac: fast tableau prover
|
changeset |
files
|
| Tue, 01 Apr 1997 18:26:09 +0200 |
wenzelm |
replaced by usedir;
|
changeset |
files
|
| Tue, 01 Apr 1997 12:54:40 +0200 |
wenzelm |
eliminated references to old 8bit fonts;
|
changeset |
files
|
| Tue, 01 Apr 1997 12:44:12 +0200 |
wenzelm |
improved messages;
|
changeset |
files
|
| Tue, 01 Apr 1997 11:16:06 +0200 |
wenzelm |
removed useless symbol font syntax;
|
changeset |
files
|
| Tue, 01 Apr 1997 09:28:56 +0200 |
wenzelm |
fixed -s option;
|
changeset |
files
|
| Mon, 31 Mar 1997 14:42:13 +0200 |
wenzelm |
simple_ast_of: fixed handling of loose Bounds;
|
changeset |
files
|
| Sun, 30 Mar 1997 13:40:38 +0200 |
nipkow |
Replaced (s,t) : id by s=t.
|
changeset |
files
|
| Thu, 27 Mar 1997 17:46:24 +0100 |
nipkow |
Optimized proofs.
|
changeset |
files
|
| Thu, 27 Mar 1997 10:08:31 +0100 |
paulson |
Changes made necessary by the new ex1 rules
|
changeset |
files
|
| Thu, 27 Mar 1997 10:07:11 +0100 |
paulson |
Now uses the alternative (safe!) rules for ex1
|
changeset |
files
|
| Thu, 27 Mar 1997 10:06:36 +0100 |
paulson |
Updated comment
|
changeset |
files
|
| Wed, 26 Mar 1997 18:51:57 +0100 |
nipkow |
Cleaned up a little.
|
changeset |
files
|
| Wed, 26 Mar 1997 17:58:48 +0100 |
nipkow |
Added "discrete" CPOs and modified IMP to use those rather than "lift"
|
changeset |
files
|
| Wed, 26 Mar 1997 13:44:05 +0100 |
slotosch |
generalized theorems and class instances for Cprod.
|
changeset |
files
|
| Tue, 25 Mar 1997 11:19:09 +0100 |
slotosch |
changed some theorems from pcpo to cpo
|
changeset |
files
|
| Tue, 25 Mar 1997 11:13:12 +0100 |
slotosch |
changed continuous functions from pcpo to cpo (including instances)
|
changeset |
files
|
| Tue, 25 Mar 1997 10:43:01 +0100 |
paulson |
Trivial renamings (for consistency with CSFW papers)
|
changeset |
files
|
| Tue, 25 Mar 1997 10:41:44 +0100 |
paulson |
Toby's better treatment of eta-contraction
|
changeset |
files
|
| Mon, 24 Mar 1997 10:28:23 +0100 |
paulson |
Deleted needless parentheses
|
changeset |
files
|
| Mon, 24 Mar 1997 10:27:28 +0100 |
paulson |
Deleted unnecessary rules
|
changeset |
files
|
| Thu, 20 Mar 1997 19:12:20 +0100 |
wenzelm |
fixed font names;
|
changeset |
files
|
| Thu, 20 Mar 1997 18:28:05 +0100 |
wenzelm |
exit_use_dir;
|
changeset |
files
|
| Thu, 20 Mar 1997 18:27:23 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 18:27:05 +0100 |
wenzelm |
exit_use_dir;
|
changeset |
files
|
| Thu, 20 Mar 1997 12:34:08 +0100 |
wenzelm |
remove empty dirs;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:39:40 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:38:58 +0100 |
wenzelm |
improved session names;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:32:57 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:31:47 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 20 Mar 1997 11:29:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:24:05 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:23:19 +0100 |
wenzelm |
exit_use_dir;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:11:53 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 11:09:01 +0100 |
wenzelm |
replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
|
changeset |
files
|
| Thu, 20 Mar 1997 10:49:44 +0100 |
wenzelm |
isatool usedir;
|
changeset |
files
|
| Thu, 20 Mar 1997 10:48:00 +0100 |
wenzelm |
added ex dir;
|
changeset |
files
|
| Thu, 20 Mar 1997 10:47:29 +0100 |
wenzelm |
replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
|
changeset |
files
|
| Thu, 20 Mar 1997 10:47:18 +0100 |
wenzelm |
replaced ex.ML by ex/ROOT.ml, ex/ex.ML;
|
changeset |
files
|
| Wed, 19 Mar 1997 10:49:26 +0100 |
paulson |
Improved intersection rule InterI: now truly safe, since the unsafeness is
|
changeset |
files
|
| Wed, 19 Mar 1997 10:24:39 +0100 |
paulson |
delete_tagged_brl just ignores non-elimination rules instead of complaining
|
changeset |
files
|
| Wed, 19 Mar 1997 10:23:09 +0100 |
paulson |
delrules now deletes ALL occurrences of a rule, since it may appear in any of
|
changeset |
files
|
| Tue, 18 Mar 1997 18:20:52 +0100 |
wenzelm |
added quit();
|
changeset |
files
|
| Tue, 18 Mar 1997 18:20:26 +0100 |
wenzelm |
asserts $ISABELLE_OUTPUT_DIR;
|
changeset |
files
|
| Tue, 18 Mar 1997 18:02:19 +0100 |
nipkow |
Added wp_while.
|
changeset |
files
|
| Tue, 18 Mar 1997 17:03:55 +0100 |
wenzelm |
added dummy set_session;
|
changeset |
files
|
| Tue, 18 Mar 1997 17:03:05 +0100 |
wenzelm |
usedir -- build object-logic or run examples;
|
changeset |
files
|
| Tue, 18 Mar 1997 15:15:01 +0100 |
paulson |
A more explicit prefix because gensym now generates easily predicatable
|
changeset |
files
|
| Tue, 18 Mar 1997 15:12:53 +0100 |
paulson |
gensym no longer generates random identifiers, but just enumerates them
|
changeset |
files
|
| Tue, 18 Mar 1997 15:11:02 +0100 |
paulson |
Made the indentation rational
|
changeset |
files
|
| Tue, 18 Mar 1997 14:35:10 +0100 |
wenzelm |
fixed Tools path;
|
changeset |
files
|
| Tue, 18 Mar 1997 10:43:29 +0100 |
paulson |
Conducted the IFOL proofs using intuitionistic tools
|
changeset |
files
|
| Tue, 18 Mar 1997 10:42:08 +0100 |
paulson |
Stopped giving Introduction rules as Elimination rules
|
changeset |
files
|
| Tue, 18 Mar 1997 08:43:26 +0100 |
nipkow |
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
|
changeset |
files
|
| Tue, 18 Mar 1997 08:42:18 +0100 |
nipkow |
Added P&P&Q = P&Q and P|P|Q = P|Q.
|
changeset |
files
|
| Mon, 17 Mar 1997 15:38:26 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 17 Mar 1997 15:37:41 +0100 |
nipkow |
The HOLCF-based den. sem. of IMP.
|
changeset |
files
|
| Mon, 17 Mar 1997 15:37:16 +0100 |
nipkow |
Added the HOLCF-based den. sem. of IMP.
|
changeset |
files
|
| Mon, 17 Mar 1997 15:09:13 +0100 |
nipkow |
Added link to HOLCF/IMP
|
changeset |
files
|
| Mon, 17 Mar 1997 12:25:22 +0100 |
wenzelm |
fixed perl path;
|
changeset |
files
|
| Mon, 17 Mar 1997 10:39:57 +0100 |
wenzelm |
uncommented chown / chmod (again);
|
changeset |
files
|
| Fri, 14 Mar 1997 10:37:01 +0100 |
nipkow |
Modified proofs because simplifier does not eta-contract any longer.
|
changeset |
files
|
| Fri, 14 Mar 1997 10:35:30 +0100 |
nipkow |
Avoid eta-contraction in the simplifier.
|
changeset |
files
|
| Tue, 11 Mar 1997 17:20:59 +0100 |
wenzelm |
tuned glyphs;
|
changeset |
files
|
| Tue, 11 Mar 1997 17:20:31 +0100 |
wenzelm |
tuned Sigma glyph;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:39:20 +0100 |
wenzelm |
major tuning;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:38:53 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:38:23 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:24:44 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:17:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 Mar 1997 16:17:01 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Tue, 11 Mar 1997 14:44:25 +0100 |
wenzelm |
Note on fonts and remote X11;
|
changeset |
files
|
| Tue, 11 Mar 1997 14:21:10 +0100 |
wenzelm |
tr is (again) type abbrev;
|
changeset |
files
|
| Tue, 11 Mar 1997 13:05:40 +0100 |
wenzelm |
added THIS_IS_ISABELLE_BUILD;
|
changeset |
files
|
| Tue, 11 Mar 1997 13:05:11 +0100 |
wenzelm |
added THIS_IS_ISABELLE_BUILD discrimination;
|
changeset |
files
|
| Mon, 10 Mar 1997 10:32:32 +0100 |
paulson |
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
|
changeset |
files
|
| Fri, 07 Mar 1997 16:44:28 +0100 |
wenzelm |
renamed;
|
changeset |
files
|
| Fri, 07 Mar 1997 16:44:14 +0100 |
wenzelm |
fixed;
|
changeset |
files
|
| Fri, 07 Mar 1997 16:40:30 +0100 |
wenzelm |
commented out chwon, chmod;
|
changeset |
files
|
| Fri, 07 Mar 1997 16:16:47 +0100 |
wenzelm |
fixed src path;
|
changeset |
files
|
| Fri, 07 Mar 1997 16:08:36 +0100 |
wenzelm |
added \n at EOF;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:51:44 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Fri, 07 Mar 1997 15:51:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:34:10 +0100 |
wenzelm |
renamed fonts;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:33:53 +0100 |
wenzelm |
renamed font;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:32:16 +0100 |
wenzelm |
removed lparr, rparr, empty, succeq, ge, rrightarrow;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:30:23 +0100 |
wenzelm |
renamed SYSTEM to RAW_ML_SYSTEM;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:29:46 +0100 |
wenzelm |
added \<Colon> syntax for constraints (more compact!);
|
changeset |
files
|
| Fri, 07 Mar 1997 15:28:22 +0100 |
wenzelm |
"bool lift" now syntax instead of type abbrev;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:23:12 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Fri, 07 Mar 1997 15:05:21 +0100 |
wenzelm |
added atac 2 (again);
|
changeset |
files
|
| Fri, 07 Mar 1997 15:05:00 +0100 |
wenzelm |
removed (| |) symbols syntax;
|
changeset |
files
|
| Fri, 07 Mar 1997 15:03:57 +0100 |
wenzelm |
fixed Not syntax;
|
changeset |
files
|
| Fri, 07 Mar 1997 14:52:19 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Fri, 07 Mar 1997 14:51:50 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 07 Mar 1997 14:49:56 +0100 |
wenzelm |
Isabelle installation notes;
|
changeset |
files
|
| Fri, 07 Mar 1997 14:31:00 +0100 |
wenzelm |
now sans serifs;
|
changeset |
files
|
| Fri, 07 Mar 1997 13:47:37 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Mar 1997 13:21:15 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Fri, 07 Mar 1997 11:49:04 +0100 |
wenzelm |
build - compile parts of the Isabelle system;
|
changeset |
files
|
| Fri, 07 Mar 1997 11:48:46 +0100 |
wenzelm |
moved settings comment to build;
|
changeset |
files
|
| Fri, 07 Mar 1997 10:26:02 +0100 |
paulson |
Removed some polymorphic equality tests
|
changeset |
files
|
| Fri, 07 Mar 1997 10:24:26 +0100 |
paulson |
Improved indentation of aconv
|
changeset |
files
|
| Fri, 07 Mar 1997 10:23:54 +0100 |
paulson |
Corrected aeconv and exported it
|
changeset |
files
|
| Fri, 07 Mar 1997 10:22:54 +0100 |
paulson |
Prevent permutation of assumptions in hyp_subst_tac
|
changeset |
files
|
| Fri, 07 Mar 1997 10:21:11 +0100 |
paulson |
Deleted steps made redundant by the stronger eq_assume_tac
|
changeset |
files
|
| Fri, 07 Mar 1997 10:20:26 +0100 |
paulson |
Eta-expanded some declarations for compatibility with value polymorphism
|
changeset |
files
|
| Fri, 07 Mar 1997 10:19:24 +0100 |
paulson |
Tidied and updated
|
changeset |
files
|
| Fri, 07 Mar 1997 09:56:55 +0100 |
wenzelm |
more robust check;
|
changeset |
files
|
| Fri, 07 Mar 1997 09:49:28 +0100 |
wenzelm |
renamed, improved, augmented version of isabelle fonts;
|
changeset |
files
|
| Fri, 07 Mar 1997 09:43:31 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Fri, 07 Mar 1997 09:43:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Mar 1997 09:42:26 +0100 |
wenzelm |
pass xterm mode by default;
|
changeset |
files
|
| Thu, 06 Mar 1997 16:06:31 +0100 |
pusch |
Minor changes due to primrec definition for ^
|
changeset |
files
|
| Thu, 06 Mar 1997 16:06:08 +0100 |
pusch |
primrec definition for ^
|
changeset |
files
|
| Thu, 06 Mar 1997 16:05:32 +0100 |
pusch |
Minor changes due to primrec definition for nth
|
changeset |
files
|
| Thu, 06 Mar 1997 16:04:23 +0100 |
pusch |
primrec definition for nth
|
changeset |
files
|
| Thu, 06 Mar 1997 12:32:58 +0100 |
wenzelm |
Oops, forgot to remove -x again;
|
changeset |
files
|
| Thu, 06 Mar 1997 12:30:32 +0100 |
wenzelm |
added ISABELLE_HOME normalization;
|
changeset |
files
|
| Thu, 06 Mar 1997 12:28:17 +0100 |
wenzelm |
even more robust and user friendly invocation (no longer requieres
|
changeset |
files
|
| Wed, 05 Mar 1997 17:15:31 +0100 |
wenzelm |
improved DESCRIPTION;
|
changeset |
files
|
| Wed, 05 Mar 1997 17:13:56 +0100 |
wenzelm |
added -a, -b options;
|
changeset |
files
|
| Wed, 05 Mar 1997 14:19:34 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Wed, 05 Mar 1997 13:40:41 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Wed, 05 Mar 1997 13:37:16 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Wed, 05 Mar 1997 10:19:42 +0100 |
paulson |
Added comment
|
changeset |
files
|
| Wed, 05 Mar 1997 10:08:32 +0100 |
paulson |
Now uses eta_contract_atom for greater speed
|
changeset |
files
|
| Wed, 05 Mar 1997 10:07:04 +0100 |
paulson |
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
|
changeset |
files
|
| Wed, 05 Mar 1997 10:05:32 +0100 |
paulson |
HOL: renaming of "not"
|
changeset |
files
|
| Wed, 05 Mar 1997 10:04:45 +0100 |
paulson |
Declares eta_contract_atom; fixed comment; some tidying
|
changeset |
files
|
| Wed, 05 Mar 1997 10:03:30 +0100 |
paulson |
Added comment
|
changeset |
files
|
| Wed, 05 Mar 1997 10:02:53 +0100 |
paulson |
Now declares needs_filtered_use, but still unusable with current MLWorks
|
changeset |
files
|
| Wed, 05 Mar 1997 10:01:57 +0100 |
paulson |
Now uses rotate_tac and eta_contract_atom for greater speed
|
changeset |
files
|
| Wed, 05 Mar 1997 09:59:55 +0100 |
paulson |
New version of InterE, like its ZF counterpart
|
changeset |
files
|
| Wed, 05 Mar 1997 09:59:24 +0100 |
paulson |
Renamed constant "not" to "Not"
|
changeset |
files
|
| Tue, 04 Mar 1997 10:58:29 +0100 |
paulson |
Renamed constant "not" to "Not"
|
changeset |
files
|
| Tue, 04 Mar 1997 10:48:36 +0100 |
paulson |
Renamed constant "not" to "Not"
|
changeset |
files
|
| Tue, 04 Mar 1997 10:42:28 +0100 |
paulson |
best_tac avoids looping with change to RepFun_eqI in claset
|
changeset |
files
|
| Tue, 04 Mar 1997 10:41:33 +0100 |
paulson |
Now uses RepFun_eqI instead of RepFunI;
|
changeset |
files
|
| Tue, 04 Mar 1997 10:21:16 +0100 |
paulson |
Updated reference to Pelletier erratum
|
changeset |
files
|
| Tue, 04 Mar 1997 10:19:38 +0100 |
paulson |
Removed needless quotes
|
changeset |
files
|
| Mon, 03 Mar 1997 18:26:33 +0100 |
wenzelm |
removed bash debug;
|
changeset |
files
|
| Mon, 03 Mar 1997 18:25:17 +0100 |
wenzelm |
removed -r option;
|
changeset |
files
|
| Mon, 03 Mar 1997 18:24:34 +0100 |
wenzelm |
fixed -m order;
|
changeset |
files
|
| Mon, 03 Mar 1997 14:14:04 +0100 |
wenzelm |
improved xterm, xterm_color;
|
changeset |
files
|
| Mon, 03 Mar 1997 13:53:29 +0100 |
wenzelm |
added comment;
|
changeset |
files
|
| Mon, 03 Mar 1997 13:50:40 +0100 |
wenzelm |
added comment: print translations do not mark tokens;
|
changeset |
files
|
| Sat, 01 Mar 1997 20:09:50 +0100 |
wenzelm |
added color styles;
|
changeset |
files
|
| Fri, 28 Feb 1997 21:54:37 +0100 |
wenzelm |
improved err msg;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:58:42 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Fri, 28 Feb 1997 16:56:31 +0100 |
wenzelm |
more robust handling of invocation errors;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:55:35 +0100 |
wenzelm |
more robust handling of invocation errors;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:54:32 +0100 |
wenzelm |
now uses -m symbols;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:47:56 +0100 |
wenzelm |
split ast_of_term(T);
|
changeset |
files
|
| Fri, 28 Feb 1997 16:46:26 +0100 |
wenzelm |
added token translation support;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:45:38 +0100 |
wenzelm |
term_of_... now mark class, tfree, tvar;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:44:30 +0100 |
wenzelm |
added mark_bound(T), variant_abs';
|
changeset |
files
|
| Fri, 28 Feb 1997 16:42:06 +0100 |
wenzelm |
Token translations for xterm and LaTeX output.
|
changeset |
files
|
| Fri, 28 Feb 1997 16:41:49 +0100 |
wenzelm |
added _mk_ofclass(S);
|
changeset |
files
|
| Fri, 28 Feb 1997 16:41:04 +0100 |
wenzelm |
added strlen (includes metric information);
|
changeset |
files
|
| Fri, 28 Feb 1997 16:40:08 +0100 |
wenzelm |
added token_translation interface;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:39:30 +0100 |
wenzelm |
added add_tokentrfuns;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:38:55 +0100 |
wenzelm |
added Syntax/token_trans.ML;
|
changeset |
files
|
| Fri, 28 Feb 1997 16:36:49 +0100 |
wenzelm |
added token_trans.ML;
|
changeset |
files
|
| Fri, 28 Feb 1997 15:52:16 +0100 |
paulson |
Slightly more robust proof
|
changeset |
files
|
| Fri, 28 Feb 1997 15:51:06 +0100 |
paulson |
dup_intr & dup_elim no longer call standard -- this
|
changeset |
files
|
| Fri, 28 Feb 1997 15:46:41 +0100 |
paulson |
rule_by_tactic no longer standardizes its result
|
changeset |
files
|
| Fri, 28 Feb 1997 15:44:32 +0100 |
paulson |
Addition of de Bruijn formulae
|
changeset |
files
|
| Thu, 27 Feb 1997 13:44:55 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Thu, 27 Feb 1997 12:10:28 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 25 Feb 1997 16:57:25 +0100 |
wenzelm |
added proper subset symbols syntax;
|
changeset |
files
|
| Tue, 25 Feb 1997 15:12:49 +0100 |
pusch |
minor changes due to primrec defintions for +,-,*
|
changeset |
files
|
| Tue, 25 Feb 1997 15:11:56 +0100 |
pusch |
minor changes due to new primrec definitions for +,-,*
|
changeset |
files
|
| Tue, 25 Feb 1997 15:11:12 +0100 |
pusch |
definitions of +,-,* replaced by primrec definitions
|
changeset |
files
|
| Tue, 25 Feb 1997 15:05:14 +0100 |
pusch |
function nat_add_primrec added to allow primrec definitions over nat
|
changeset |
files
|
| Mon, 24 Feb 1997 16:12:24 +0100 |
oheimb |
removed explicit_domains/, which is now covered by ex/
|
changeset |
files
|
| Mon, 24 Feb 1997 09:46:12 +0100 |
wenzelm |
added "_" syntax for dummyT;
|
changeset |
files
|
| Fri, 21 Feb 1997 16:43:04 +0100 |
wenzelm |
declared the dummy type;
|
changeset |
files
|
| Fri, 21 Feb 1997 16:35:49 +0100 |
wenzelm |
replaced natural by subset;
|
changeset |
files
|
| Fri, 21 Feb 1997 16:35:30 +0100 |
wenzelm |
tuned symbolic [|_|] syntax;
|
changeset |
files
|
| Fri, 21 Feb 1997 16:28:00 +0100 |
wenzelm |
tuned some chars;
|
changeset |
files
|
| Fri, 21 Feb 1997 15:38:44 +0100 |
paulson |
More robust proof (?)
|
changeset |
files
|
| Fri, 21 Feb 1997 15:31:47 +0100 |
paulson |
Replaced "flat" by the Basis Library function List.concat
|
changeset |
files
|
| Fri, 21 Feb 1997 15:30:41 +0100 |
paulson |
Introduction of rotate_rule
|
changeset |
files
|
| Fri, 21 Feb 1997 15:15:26 +0100 |
wenzelm |
removed empty line (which broke xfedor);
|
changeset |
files
|
| Fri, 21 Feb 1997 15:14:16 +0100 |
wenzelm |
don't hack, use xfed or xfedor;
|
changeset |
files
|
| Fri, 21 Feb 1997 11:18:33 +0100 |
wenzelm |
fixed Id comment;
|
changeset |
files
|
| Thu, 20 Feb 1997 17:02:42 +0100 |
wenzelm |
makedist -- make Isabelle distribution.
|
changeset |
files
|
| Thu, 20 Feb 1997 16:45:47 +0100 |
wenzelm |
tuned URL;
|
changeset |
files
|
| Thu, 20 Feb 1997 16:09:41 +0100 |
wenzelm |
added index info;
|
changeset |
files
|