| Fri, 19 Dec 1997 12:16:32 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 19 Dec 1997 12:09:58 +0100 | wenzelm | new version; | changeset | files |
| Fri, 19 Dec 1997 12:09:08 +0100 | wenzelm | added record.ML; | changeset | files |
| Fri, 19 Dec 1997 12:00:24 +0100 | narasche | first version of records | changeset | files |
| Fri, 19 Dec 1997 10:33:59 +0100 | wenzelm | pasted old insertion sort (does not work with new sort function!) | changeset | files |
| Fri, 19 Dec 1997 10:33:24 +0100 | wenzelm | adapted to new sort function; | changeset | files |
| Fri, 19 Dec 1997 10:31:13 +0100 | wenzelm | log file; | changeset | files |
| Fri, 19 Dec 1997 10:30:27 +0100 | wenzelm | leading 0s; | changeset | files |
| Fri, 19 Dec 1997 10:28:33 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 19 Dec 1997 10:27:23 +0100 | wenzelm | adapted to new sort function; | changeset | files |
| Fri, 19 Dec 1997 10:18:58 +0100 | wenzelm | log files; | changeset | files |
| Fri, 19 Dec 1997 10:18:03 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 19 Dec 1997 10:17:04 +0100 | wenzelm | added rev_order, make_ord; | changeset | files |
| Fri, 19 Dec 1997 10:16:16 +0100 | wenzelm | term order; | changeset | files |
| Fri, 19 Dec 1997 10:15:51 +0100 | wenzelm | term order stuff moved to term.ML; | changeset | files |
| Fri, 19 Dec 1997 10:15:26 +0100 | wenzelm | log file; | changeset | files |
| Fri, 19 Dec 1997 10:14:55 +0100 | wenzelm | 'clean' target; | changeset | files |
| Fri, 19 Dec 1997 10:13:47 +0100 | wenzelm | adapted to new sort function; | changeset | files |
| Fri, 19 Dec 1997 09:58:42 +0100 | wenzelm | Term.termless; | changeset | files |
| Fri, 19 Dec 1997 09:58:03 +0100 | wenzelm | adapted to new sort function; | changeset | files |
| Fri, 19 Dec 1997 09:57:24 +0100 | wenzelm | removed maketest; | changeset | files |
| Thu, 18 Dec 1997 19:12:22 +0100 | wenzelm | showtime - print time. | changeset | files |
| Thu, 18 Dec 1997 12:50:58 +0100 | oheimb | added expand_split_asm | changeset | files |
| Thu, 18 Dec 1997 11:13:10 +0100 | paulson | UNIV_I no longer counts as safe | changeset | files |
| Wed, 17 Dec 1997 18:13:43 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 17 Dec 1997 17:59:18 +0100 | wenzelm | added mlworks; | changeset | files |
| Wed, 17 Dec 1997 17:51:39 +0100 | wenzelm | added MLWorks; | changeset | files |
| Wed, 17 Dec 1997 15:43:54 +0100 | wenzelm | misc improvements; | changeset | files |
| Wed, 17 Dec 1997 15:43:22 +0100 | wenzelm | tuned tmp file name; | changeset | files |
| Wed, 17 Dec 1997 14:57:26 +0100 | wenzelm | tuned comment; | changeset | files |
| Wed, 17 Dec 1997 14:57:02 +0100 | wenzelm | added ML-Systems/mlworks.ML; | changeset | files |
| Tue, 16 Dec 1997 19:00:38 +0100 | wenzelm | MLWorks startup script (for 1.0r2 or later). | changeset | files |
| Tue, 16 Dec 1997 18:58:33 +0100 | wenzelm | renamed to mlworks.ML; | changeset | files |
| Tue, 16 Dec 1997 18:58:16 +0100 | wenzelm | Compatibility file for MLWorks version 1.0r2 or later. | changeset | files |
| Tue, 16 Dec 1997 17:58:03 +0100 | wenzelm | expandshort; | changeset | files |
| Tue, 16 Dec 1997 15:17:26 +0100 | paulson | Simplified proofs using rewrites for f``A where f is injective | changeset | files |
| Tue, 16 Dec 1997 15:15:38 +0100 | paulson | Simplified SpyKeys and ClientKeyExch as suggested by James Margetson | changeset | files |
| Tue, 16 Dec 1997 12:37:11 +0100 | wenzelm | obsolete; | changeset | files |
| Tue, 16 Dec 1997 12:24:31 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 16 Dec 1997 12:19:26 +0100 | wenzelm | obsolete; | changeset | files |
| Tue, 16 Dec 1997 12:17:48 +0100 | wenzelm | adapted from Larry's version; | changeset | files |
| Tue, 16 Dec 1997 12:17:22 +0100 | wenzelm | improved; | changeset | files |
| Mon, 15 Dec 1997 15:54:47 +0100 | wenzelm | improved COMMIT_RO; | changeset | files |
| Mon, 15 Dec 1997 15:32:27 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 15 Dec 1997 15:27:03 +0100 | wenzelm | polyml-3.1; | changeset | files |
| Mon, 15 Dec 1997 15:18:46 +0100 | wenzelm | make smlnj-110 default; | changeset | files |
| Mon, 15 Dec 1997 15:16:43 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 15 Dec 1997 14:40:13 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 15 Dec 1997 14:14:06 +0100 | wenzelm | No longer depend on theory context! | changeset | files |
| Sat, 13 Dec 1997 17:27:16 +0100 | wenzelm | version = "Isabelle98: Jan 1998"; | changeset | files |
| Sat, 13 Dec 1997 17:22:41 +0100 | wenzelm | tuned comment; | changeset | files |
| Sat, 13 Dec 1997 17:22:15 +0100 | wenzelm | smlnj-110; | changeset | files |
| Fri, 12 Dec 1997 22:43:10 +0100 | wenzelm | deleted smlnj-1.09.ML; | changeset | files |
| Fri, 12 Dec 1997 22:41:45 +0100 | wenzelm | obsolete; | changeset | files |
| Fri, 12 Dec 1997 22:41:15 +0100 | wenzelm | Compatibility file for Standard ML of New Jersey. | changeset | files |
| Fri, 12 Dec 1997 22:35:34 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 12 Dec 1997 18:10:59 +0100 | wenzelm | prepared for Isabelle98; | changeset | files |
| Fri, 12 Dec 1997 17:51:45 +0100 | wenzelm | added; | changeset | files |
| Fri, 12 Dec 1997 17:50:28 +0100 | wenzelm | obsolete; | changeset | files |
| Fri, 12 Dec 1997 17:23:01 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 12 Dec 1997 17:14:58 +0100 | wenzelm | tuned msg; | changeset | files |
| Fri, 12 Dec 1997 17:11:26 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 12 Dec 1997 17:11:05 +0100 | wenzelm | major update; | changeset | files |
| Fri, 12 Dec 1997 17:10:40 +0100 | wenzelm | SYNC; | changeset | files |
| Fri, 12 Dec 1997 10:46:09 +0100 | paulson | new blast_tac no longer works here | changeset | files |
| Fri, 12 Dec 1997 10:37:45 +0100 | paulson | More deterministic (?) contr_tac | changeset | files |
| Fri, 12 Dec 1997 10:34:21 +0100 | paulson | More deterministic and therefore faster (sometimes) proof reconstruction | changeset | files |
| Fri, 12 Dec 1997 10:32:45 +0100 | paulson | ugly patch for new Blast_tac | changeset | files |
| Fri, 12 Dec 1997 10:31:25 +0100 | paulson | Faster proof of mult_less_cancel2 | changeset | files |
| Thu, 11 Dec 1997 13:15:06 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 11 Dec 1997 10:30:33 +0100 | paulson | Tidied final proof | changeset | files |
| Thu, 11 Dec 1997 10:29:22 +0100 | paulson | Tidied proof of finite_subset_induct | changeset | files |
| Thu, 11 Dec 1997 10:28:04 +0100 | paulson | Got rid of mod2_neq_0 | changeset | files |
| Mon, 08 Dec 1997 20:29:49 +0100 | wenzelm | \subsection{*Theory inclusion}; | changeset | files |
| Mon, 08 Dec 1997 13:57:19 +0100 | paulson | Tidying to fix overfull lines, etc | changeset | files |
| Mon, 08 Dec 1997 13:56:49 +0100 | paulson | Comprehensive (??) list of bugs, fixed or not | changeset | files |
| Sun, 07 Dec 1997 16:09:55 +0100 | wenzelm | tuned; | changeset | files |
| Sun, 07 Dec 1997 16:05:36 +0100 | wenzelm | added print_claset; | changeset | files |
| Sat, 06 Dec 1997 17:06:21 +0100 | nipkow | Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)). | changeset | files |
| Sat, 06 Dec 1997 17:05:41 +0100 | nipkow | Got rid of some preds and replaced some n~=0 by 0<n. | changeset | files |
| Sat, 06 Dec 1997 16:48:39 +0100 | nipkow | Cleaned up arithmetic mess. | changeset | files |
| Fri, 05 Dec 1997 18:46:18 +0100 | wenzelm | instantiate'; | changeset | files |
| Fri, 05 Dec 1997 18:45:19 +0100 | wenzelm | changed typed_print_translation; | changeset | files |
| Fri, 05 Dec 1997 18:44:56 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 05 Dec 1997 17:31:01 +0100 | wenzelm | nat_cancel enabled by default; | changeset | files |
| Fri, 05 Dec 1997 17:20:25 +0100 | wenzelm | adapted proofs to cope with simprocs nat_cancel; | changeset | files |
| Fri, 05 Dec 1997 17:19:38 +0100 | wenzelm | improved arbitrary_def: we now really don't know nothing about it! | changeset | files |
| Fri, 05 Dec 1997 17:16:22 +0100 | wenzelm | use_thy no longer requires writable current directory; | changeset | files |
| Fri, 05 Dec 1997 17:14:36 +0100 | wenzelm | adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer); | changeset | files |
| Fri, 05 Dec 1997 17:13:46 +0100 | wenzelm | simplification procedures nat_cancel enabled by default; | changeset | files |
| Fri, 05 Dec 1997 08:01:03 +0100 | wenzelm | tmp_name; | changeset | files |
| Thu, 04 Dec 1997 14:11:37 +0100 | wenzelm | added print_simpset; | changeset | files |
| Thu, 04 Dec 1997 13:50:43 +0100 | wenzelm | added is_base; | changeset | files |
| Thu, 04 Dec 1997 13:50:18 +0100 | wenzelm | added reset_context; | changeset | files |
| Thu, 04 Dec 1997 13:49:51 +0100 | wenzelm | added eq_set; | changeset | files |
| Thu, 04 Dec 1997 13:49:27 +0100 | wenzelm | moved global_names ref to Pure/ROOT.ML; | changeset | files |
| Thu, 04 Dec 1997 12:50:02 +0100 | nipkow | pred -> -1 | changeset | files |
| Thu, 04 Dec 1997 12:44:37 +0100 | nipkow | pred n -> n-1 | changeset | files |
| Thu, 04 Dec 1997 09:05:59 +0100 | nipkow | Simplified proofs. | changeset | files |
| Thu, 04 Dec 1997 09:05:39 +0100 | nipkow | Added thm mult_div_cancel | changeset | files |
| Wed, 03 Dec 1997 17:31:25 +0100 | nipkow | n ~= 0 should become 0 < n | changeset | files |
| Wed, 03 Dec 1997 17:25:43 +0100 | nipkow | Replaced n ~= 0 by 0 < n | changeset | files |
| Wed, 03 Dec 1997 12:55:04 +0100 | wenzelm | pass return code!! | changeset | files |
| Wed, 03 Dec 1997 11:42:45 +0100 | paulson | Fixed the treatment of substitution for equations, restricting occurrences of | changeset | files |
| Wed, 03 Dec 1997 11:00:24 +0100 | paulson | updated for latest Blast_tac, which treats equality differently | changeset | files |
| Wed, 03 Dec 1997 10:52:17 +0100 | paulson | Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML | changeset | files |
| Wed, 03 Dec 1997 10:50:02 +0100 | paulson | Tidying and some comments | changeset | files |
| Wed, 03 Dec 1997 10:49:33 +0100 | paulson | updated for latest Blast_tac, which treats equality differently | changeset | files |
| Wed, 03 Dec 1997 10:48:16 +0100 | paulson | Instantiated the one-point-rule quantifier simpprocs for FOL | changeset | files |
| Wed, 03 Dec 1997 10:47:13 +0100 | paulson | updated for latest Blast_tac, which fixes an equality bug | changeset | files |
| Wed, 03 Dec 1997 10:45:42 +0100 | paulson | Miniscoping now used except for one proof | changeset | files |
| Tue, 02 Dec 1997 12:42:59 +0100 | wenzelm | adapted to new term order; | changeset | files |
| Tue, 02 Dec 1997 12:42:28 +0100 | wenzelm | tuned term order; | changeset | files |
| Tue, 02 Dec 1997 12:41:29 +0100 | wenzelm | tuned trfuns types; | changeset | files |
| Tue, 02 Dec 1997 12:41:02 +0100 | wenzelm | added prod_ord, dict_ord, list_ord; | changeset | files |
| Tue, 02 Dec 1997 12:40:06 +0100 | wenzelm | File.tmp_name; | changeset | files |
| Tue, 02 Dec 1997 12:39:03 +0100 | wenzelm | added tmp_name; | changeset | files |
| Tue, 02 Dec 1997 12:38:39 +0100 | wenzelm | ISABELLE_TMP; | changeset | files |
| Tue, 02 Dec 1997 12:38:08 +0100 | wenzelm | added context.ML; | changeset | files |
| Tue, 02 Dec 1997 12:37:44 +0100 | wenzelm | Global contexts: session and theory. | changeset | files |
| Tue, 02 Dec 1997 12:37:22 +0100 | wenzelm | added Thy/context.ML; | changeset | files |
| Mon, 01 Dec 1997 18:27:43 +0100 | wenzelm | open; | changeset | files |
| Mon, 01 Dec 1997 18:27:06 +0100 | wenzelm | nat_cancel simprocs; | changeset | files |
| Mon, 01 Dec 1997 18:22:38 +0100 | wenzelm | ISABELLE_TMP_PREFIX; | changeset | files |
| Mon, 01 Dec 1997 18:22:02 +0100 | wenzelm | ISABELLE_TMP; | changeset | files |
| Mon, 01 Dec 1997 14:42:30 +0100 | berghofe | Added DiffCancelSums. | changeset | files |
| Mon, 01 Dec 1997 12:52:18 +0100 | paulson | New guarantee B_trusts_NS5, and tidying | changeset | files |
| Mon, 01 Dec 1997 12:50:04 +0100 | paulson | speed-up | changeset | files |
| Mon, 01 Dec 1997 08:59:40 +0100 | narasche | args for record data | changeset | files |
| Fri, 28 Nov 1997 16:17:30 +0100 | nipkow | Removed "open Mutil;" | changeset | files |
| Fri, 28 Nov 1997 11:00:42 +0100 | paulson | Added comments | changeset | files |
| Fri, 28 Nov 1997 10:59:14 +0100 | paulson | New timing functions startTiming and endTiming | changeset | files |
| Fri, 28 Nov 1997 10:54:13 +0100 | paulson | addsplits now in FOL, ZF too | changeset | files |
| Fri, 28 Nov 1997 10:52:32 +0100 | paulson | New example | changeset | files |
| Fri, 28 Nov 1997 10:52:04 +0100 | paulson | Printing of statistics including time for search & reconstruction | changeset | files |
| Fri, 28 Nov 1997 10:36:08 +0100 | paulson | New example | changeset | files |
| Fri, 28 Nov 1997 07:41:24 +0100 | nipkow | Removed dead code. | changeset | files |
| Fri, 28 Nov 1997 07:37:06 +0100 | nipkow | Moved the quantifier elimination simp procs into Provers. | changeset | files |
| Fri, 28 Nov 1997 07:35:47 +0100 | nipkow | Quantifier elimination procs. | changeset | files |
| Fri, 28 Nov 1997 07:35:10 +0100 | nipkow | Fixed the definition of `termord': is now antisymmetric. | changeset | files |
| Thu, 27 Nov 1997 19:39:02 +0100 | wenzelm | several minor updates; | changeset | files |
| Thu, 27 Nov 1997 19:37:36 +0100 | wenzelm | SYNC; | changeset | files |
| Thu, 27 Nov 1997 19:36:51 +0100 | wenzelm | removed read_cterms; | changeset | files |
| Thu, 27 Nov 1997 19:36:31 +0100 | wenzelm | fixed warning; | changeset | files |
| Thu, 27 Nov 1997 19:36:08 +0100 | wenzelm | removed same_thm; | changeset | files |
| Thu, 27 Nov 1997 14:05:25 +0100 | paulson | Tidying, mostly indentation | changeset | files |
| Thu, 27 Nov 1997 13:58:51 +0100 | paulson | Deleted some needless addSIs; got rid of a slow Blast_tac | changeset | files |
| Thu, 27 Nov 1997 13:38:06 +0100 | wenzelm | mk_norm_sum; | changeset | files |
| Wed, 26 Nov 1997 17:52:53 +0100 | wenzelm | separate lists of simprocs; | changeset | files |
| Wed, 26 Nov 1997 17:35:46 +0100 | paulson | Added rule impCE' | changeset | files |
| Wed, 26 Nov 1997 17:35:08 +0100 | paulson | Blast_tac can prove Pelletier\'s problem 46\! | changeset | files |
| Wed, 26 Nov 1997 17:32:52 +0100 | paulson | Tidying and using equalityCE instead of the slower equalityE | changeset | files |
| Wed, 26 Nov 1997 17:31:02 +0100 | paulson | The change from iffE to iffCE means fewer case splits in most cases. Very few | changeset | files |
| Wed, 26 Nov 1997 17:27:34 +0100 | paulson | Tidying | changeset | files |
| Wed, 26 Nov 1997 17:26:12 +0100 | paulson | Tidying and modification to cope with iffCE | changeset | files |
| Wed, 26 Nov 1997 17:23:18 +0100 | paulson | Added rule impCE' | changeset | files |
| Wed, 26 Nov 1997 17:16:48 +0100 | paulson | Changes to AddIs improve performance of Blast_tac | changeset | files |
| Wed, 26 Nov 1997 16:49:54 +0100 | paulson | Statistics | changeset | files |
| Wed, 26 Nov 1997 16:49:07 +0100 | paulson | updated comment | changeset | files |
| Wed, 26 Nov 1997 16:48:11 +0100 | paulson | Tidying and modification to cope with iffCE | changeset | files |
| Wed, 26 Nov 1997 16:45:54 +0100 | wenzelm | added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1; | changeset | files |
| Wed, 26 Nov 1997 16:44:47 +0100 | wenzelm | added Arith provers; | changeset | files |
| Wed, 26 Nov 1997 16:44:25 +0100 | wenzelm | Setup various arithmetic proof procedures. | changeset | files |
| Wed, 26 Nov 1997 16:43:42 +0100 | wenzelm | added dest_nat; | changeset | files |
| Wed, 26 Nov 1997 16:42:56 +0100 | wenzelm | moved to Arith/; | changeset | files |
| Wed, 26 Nov 1997 16:42:37 +0100 | wenzelm | Cancel common constant factor from balanced exression. | changeset | files |
| Wed, 26 Nov 1997 16:42:19 +0100 | wenzelm | Cancel common summands of balanced expressions. | changeset | files |
| Wed, 26 Nov 1997 16:41:51 +0100 | wenzelm | removed conv_prover; | changeset | files |
| Wed, 26 Nov 1997 16:41:25 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 26 Nov 1997 16:38:04 +0100 | wenzelm | added crep_cterm; | changeset | files |
| Wed, 26 Nov 1997 16:37:43 +0100 | wenzelm | fixed type of thms_containing; | changeset | files |
| Wed, 26 Nov 1997 16:37:17 +0100 | wenzelm | added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; | changeset | files |
| Wed, 26 Nov 1997 16:35:39 +0100 | wenzelm | cleaned signature; | changeset | files |
| Wed, 26 Nov 1997 16:34:13 +0100 | wenzelm | removed merge_opts; | changeset | files |
| Tue, 25 Nov 1997 17:56:49 +0100 | mueller | managed merge details; | changeset | files |
| Tue, 25 Nov 1997 16:34:20 +0100 | mueller | resolved merge conflict; | changeset | files |
| Mon, 24 Nov 1997 16:43:43 +0100 | nipkow | Added read_def_cterms for simultaneous reading/typing of terms under | changeset | files |
| Sat, 22 Nov 1997 13:27:02 +0100 | wenzelm | fixed warning; | changeset | files |
| Sat, 22 Nov 1997 13:26:43 +0100 | wenzelm | made SML/NJ happy; | changeset | files |
| Sat, 22 Nov 1997 13:26:30 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 21 Nov 1997 15:47:39 +0100 | wenzelm | replaced by seq.ML; | changeset | files |
| Fri, 21 Nov 1997 15:41:27 +0100 | wenzelm | changed Pure/Sequence interface; | changeset | files |
| Fri, 21 Nov 1997 15:40:56 +0100 | wenzelm | SYNC; | changeset | files |
| Fri, 21 Nov 1997 15:37:02 +0100 | wenzelm | cd, use: path variables; | changeset | files |
| Fri, 21 Nov 1997 15:35:37 +0100 | wenzelm | comment; | changeset | files |
| Fri, 21 Nov 1997 15:34:15 +0100 | wenzelm | obsolete; | changeset | files |
| Fri, 21 Nov 1997 15:29:56 +0100 | wenzelm | changed Pure/Sequence interface -- isatool fixseq; | changeset | files |
| Fri, 21 Nov 1997 15:27:43 +0100 | wenzelm | changed Sequence interface (now Seq, in seq.ML); | changeset | files |
| Fri, 21 Nov 1997 15:26:22 +0100 | wenzelm | cd, use etc. now support path variables; | changeset | files |
| Fri, 21 Nov 1997 13:54:31 +0100 | wenzelm | fix references to obsolete Pure/Sequence structure; | changeset | files |
| Fri, 21 Nov 1997 12:15:27 +0100 | paulson | tidying | changeset | files |
| Fri, 21 Nov 1997 12:15:10 +0100 | paulson | analz_mono_contra_tac was wrong | changeset | files |
| Fri, 21 Nov 1997 12:14:47 +0100 | paulson | Deleted some useless comments | changeset | files |
| Fri, 21 Nov 1997 11:57:58 +0100 | oheimb | minor improvements of formulation and proofs | changeset | files |
| Fri, 21 Nov 1997 11:54:23 +0100 | oheimb | corrected INDUCT_FILES | changeset | files |
| Thu, 20 Nov 1997 16:24:05 +0100 | wenzelm | $ISABELLE_HOME/src; | changeset | files |
| Thu, 20 Nov 1997 15:48:32 +0100 | wenzelm | improved error msg; | changeset | files |
| Thu, 20 Nov 1997 15:38:51 +0100 | wenzelm | removed old note; | changeset | files |
| Thu, 20 Nov 1997 15:36:09 +0100 | wenzelm | adapted print methods; | changeset | files |
| Thu, 20 Nov 1997 15:30:37 +0100 | wenzelm | improved theorems print method: transfer_sg; | changeset | files |
| Thu, 20 Nov 1997 15:30:03 +0100 | wenzelm | init_data: improved print method; | changeset | files |
| Thu, 20 Nov 1997 15:28:48 +0100 | wenzelm | removed data.ML (made part of sign.ML); | changeset | files |
| Thu, 20 Nov 1997 15:07:19 +0100 | wenzelm | added type object = exn; | changeset | files |
| Thu, 20 Nov 1997 15:06:57 +0100 | wenzelm | added transfer_sg; | changeset | files |
| Thu, 20 Nov 1997 13:00:50 +0100 | wenzelm | fixed xstr token encoding; | changeset | files |
| Thu, 20 Nov 1997 12:59:20 +0100 | wenzelm | tuned infer_types interface; | changeset | files |
| Thu, 20 Nov 1997 12:51:55 +0100 | wenzelm | tuned infer_types interface; | changeset | files |
| Thu, 20 Nov 1997 12:51:31 +0100 | wenzelm | moved Sign.print_sg to display.ML; | changeset | files |
| Thu, 20 Nov 1997 12:50:57 +0100 | wenzelm | exported pretty_classrel, pretty_arity; | changeset | files |
| Thu, 20 Nov 1997 12:49:25 +0100 | wenzelm | added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; | changeset | files |
| Thu, 20 Nov 1997 12:48:00 +0100 | wenzelm | added implode_xstr: string list -> string, explode_xstr: string -> string list; | changeset | files |
| Thu, 20 Nov 1997 11:55:39 +0100 | paulson | Now uses induct_tac | changeset | files |
| Thu, 20 Nov 1997 11:54:31 +0100 | paulson | Updated the NatSum example | changeset | files |
| Thu, 20 Nov 1997 11:53:51 +0100 | paulson | New, higher-level definition of \\out macro | changeset | files |
| Thu, 20 Nov 1997 11:03:53 +0100 | paulson | Speeded up the proof of succ_lt_induct_lemma | changeset | files |
| Thu, 20 Nov 1997 11:03:26 +0100 | paulson | Two new rewrites | changeset | files |
| Thu, 20 Nov 1997 10:55:27 +0100 | paulson | Got rid of some slow deepen_tac calls | changeset | files |
| Thu, 20 Nov 1997 10:54:04 +0100 | paulson | Renamed "overload" to "overloaded" for sml/nj compatibility | changeset | files |
| Thu, 20 Nov 1997 10:50:51 +0100 | paulson | No more makeatletter/other | changeset | files |
| Tue, 18 Nov 1997 16:37:25 +0100 | paulson | Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys | changeset | files |
| Tue, 18 Nov 1997 16:36:33 +0100 | paulson | The dtac was discarding information, though apparently no proofs were hurt | changeset | files |
| Tue, 18 Nov 1997 15:30:50 +0100 | berghofe | Fixed bug in inst_split. | changeset | files |
| Mon, 17 Nov 1997 15:40:25 +0100 | wenzelm | improved big_rec_name lookup; | changeset | files |
| Mon, 17 Nov 1997 10:50:03 +0100 | paulson | Updated comments. A bug causes MLWorks to use much | changeset | files |
| Mon, 17 Nov 1997 10:48:07 +0100 | paulson | Rationalized error handling: if low-level tactic (depth_tac) cannot accept the | changeset | files |
| Mon, 17 Nov 1997 09:52:20 +0100 | berghofe | Tuned function mk_cntxt_splitthm. | changeset | files |
| Sun, 16 Nov 1997 16:18:31 +0100 | nipkow | Removed | changeset | files |
| Sat, 15 Nov 1997 18:41:06 +0100 | nipkow | Redesigned the decision procedures for (Abelian) groups and commutative rings. | changeset | files |
| Sat, 15 Nov 1997 13:10:52 +0100 | nipkow | Added | changeset | files |
| Fri, 14 Nov 1997 15:51:09 +0100 | wenzelm | merge_refs: check for different versions of theories; | changeset | files |
| Thu, 13 Nov 1997 17:55:27 +0100 | wenzelm | export read_raw_typ; | changeset | files |
| Thu, 13 Nov 1997 15:14:14 +0100 | wenzelm | fixed record parser; | changeset | files |
| Thu, 13 Nov 1997 12:43:17 +0100 | wenzelm | improved record syntax; | changeset | files |
| Thu, 13 Nov 1997 10:31:42 +0100 | wenzelm | made SML/NJ happy; | changeset | files |
| Wed, 12 Nov 1997 18:58:50 +0100 | oheimb | added thin_refl to hyp_subst_tac | changeset | files |
| Wed, 12 Nov 1997 16:28:53 +0100 | wenzelm | refer to $ISABELLE_HOME/src; | changeset | files |
| Wed, 12 Nov 1997 16:27:13 +0100 | wenzelm | structure BasisLibrary; | changeset | files |
| Wed, 12 Nov 1997 16:26:05 +0100 | wenzelm | renamed to use.ML; | changeset | files |
| Wed, 12 Nov 1997 16:25:45 +0100 | wenzelm | Redefine 'use' command in order to support path variable expansion, | changeset | files |
| Wed, 12 Nov 1997 16:25:35 +0100 | wenzelm | adapted to new Use, File structs; | changeset | files |
| Wed, 12 Nov 1997 16:23:28 +0100 | wenzelm | added path variables; | changeset | files |
| Wed, 12 Nov 1997 16:23:11 +0100 | wenzelm | File system operations. | changeset | files |
| Wed, 12 Nov 1997 16:22:59 +0100 | wenzelm | moved old file stuff from library.ML to Thy/browser_info.ML; | changeset | files |
| Wed, 12 Nov 1997 16:22:47 +0100 | wenzelm | added file.ML, use.ML; | changeset | files |
| Wed, 12 Nov 1997 16:22:10 +0100 | wenzelm | tuned warning msg; | changeset | files |
| Wed, 12 Nov 1997 16:21:57 +0100 | wenzelm | major cleanup; | changeset | files |
| Wed, 12 Nov 1997 16:21:26 +0100 | wenzelm | moved 'latex' from library.ML to goals.ML; | changeset | files |
| Wed, 12 Nov 1997 16:21:15 +0100 | wenzelm | tuned prths; | changeset | files |
| Wed, 12 Nov 1997 16:20:49 +0100 | wenzelm | structure BasisLibrary; | changeset | files |
| Wed, 12 Nov 1997 16:20:39 +0100 | wenzelm | added Thy/file.ML, Thy/use.ML; | changeset | files |
| Wed, 12 Nov 1997 12:38:12 +0100 | oheimb | renamed split_prem_tac to split_asm_tac | changeset | files |
| Wed, 12 Nov 1997 12:34:43 +0100 | oheimb | restored last version | changeset | files |
| Wed, 12 Nov 1997 12:30:15 +0100 | oheimb | simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm | changeset | files |
| Wed, 12 Nov 1997 12:24:55 +0100 | oheimb | renamed split_T_case_prem to split_T_case_asm | changeset | files |
| Wed, 12 Nov 1997 12:23:37 +0100 | oheimb | renamed split_prem_tac to split_asm_tac | changeset | files |
| Wed, 12 Nov 1997 12:22:56 +0100 | oheimb | renamed split_prem_tac to split_asm_tac | changeset | files |