| Mon, 16 Aug 2004 14:21:54 +0200 | nipkow | *** empty log message *** | changeset | files |
| Mon, 16 Aug 2004 12:29:09 +0200 | berghofe | Replaced `div and `mod in consts_code section by div and mod. | changeset | files |
| Sat, 14 Aug 2004 16:27:56 +0200 | webertj | bugfix in read_dimacs_cnf_file | changeset | files |
| Thu, 12 Aug 2004 10:01:09 +0200 | ballarin | Disallowed "includes" in locale declarations. | changeset | files |
| Tue, 10 Aug 2004 19:10:39 +0200 | berghofe | Fixed bug in compile_clause that caused equality constraints | changeset | files |
| Mon, 09 Aug 2004 15:27:27 +0200 | webertj | warning for recursion over IDTs added | changeset | files |
| Mon, 09 Aug 2004 10:09:44 +0200 | nipkow | Aded a thm. | changeset | files |
| Fri, 06 Aug 2004 17:29:24 +0200 | chaieb | *** empty log message *** | changeset | files |
| Fri, 06 Aug 2004 17:19:50 +0200 | chaieb | proof_of_evalc corrected; | changeset | files |
| Fri, 06 Aug 2004 17:07:04 +0200 | nipkow | Initial changes to extend arithmetic from individual types to type classes. | changeset | files |
| Fri, 06 Aug 2004 16:55:14 +0200 | nipkow | undid UN/INT syntax | changeset | files |
| Fri, 06 Aug 2004 16:54:26 +0200 | nipkow | undid UN/INT xsymbol syntax with subscripts. | changeset | files |
| Fri, 06 Aug 2004 13:36:04 +0200 | paulson | make_clauses now meta | changeset | files |
| Fri, 06 Aug 2004 13:35:44 +0200 | paulson | RS -> THEN | changeset | files |
| Fri, 06 Aug 2004 13:35:26 +0200 | paulson | modified resolution proof | changeset | files |
| Fri, 06 Aug 2004 12:30:31 +0200 | nipkow | Undid \Union syntax with subscripts. | changeset | files |
| Thu, 05 Aug 2004 10:51:30 +0200 | paulson | an updated treatment of the simprules | changeset | files |
| Thu, 05 Aug 2004 10:50:58 +0200 | paulson | some structured proofs | changeset | files |
| Wed, 04 Aug 2004 19:12:15 +0200 | nipkow | added a thm | changeset | files |
| Wed, 04 Aug 2004 19:11:02 +0200 | nipkow | added some inj_on thms | changeset | files |
| Wed, 04 Aug 2004 19:10:45 +0200 | nipkow | Added a number of new thms and the new function remove1 | changeset | files |
| Wed, 04 Aug 2004 19:09:58 +0200 | nipkow | proof mod | changeset | files |
| Wed, 04 Aug 2004 19:09:41 +0200 | nipkow | added a few thms | changeset | files |
| Wed, 04 Aug 2004 17:43:55 +0200 | chaieb | oracle corrected | changeset | files |
| Wed, 04 Aug 2004 11:25:08 +0200 | nipkow | aded comment | changeset | files |
| Wed, 04 Aug 2004 09:44:40 +0200 | nipkow | fixed tex problem | changeset | files |
| Tue, 03 Aug 2004 14:48:59 +0200 | ballarin | Typo. | changeset | files |
| Tue, 03 Aug 2004 14:47:51 +0200 | ballarin | New transitivity reasoners for transitivity only and quasi orders. | changeset | files |
| Tue, 03 Aug 2004 13:48:00 +0200 | paulson | new simprules Int_subset_iff and Un_subset_iff | changeset | files |
| Mon, 02 Aug 2004 16:06:13 +0200 | obua | zdiv_int, zmod_int | changeset | files |
| Mon, 02 Aug 2004 11:20:37 +0200 | paulson | conversion of Hyperreal/Filter to Isar scripts | changeset | files |
| Mon, 02 Aug 2004 10:16:58 +0200 | ballarin | Some comments added. | changeset | files |
| Mon, 02 Aug 2004 10:16:40 +0200 | ballarin | Documentation added/improved. | changeset | files |
| Mon, 02 Aug 2004 10:15:37 +0200 | ballarin | Modifications for trancl_tac (new solver in simplifier). | changeset | files |
| Mon, 02 Aug 2004 10:12:02 +0200 | ballarin | Documentation added; minor improvements. | changeset | files |
| Mon, 02 Aug 2004 09:44:46 +0200 | ballarin | Theories now take advantage of recent syntax improvements with (structure). | changeset | files |
| Sat, 31 Jul 2004 20:54:23 +0200 | paulson | conversion of Hyperreal/{Fact,Filter} to Isar scripts | changeset | files |
| Fri, 30 Jul 2004 18:37:58 +0200 | paulson | conversion of Integration and NSPrimes to Isar scripts | changeset | files |
| Fri, 30 Jul 2004 10:44:42 +0200 | wenzelm | keep type_solver; | changeset | files |
| Fri, 30 Jul 2004 10:44:34 +0200 | wenzelm | tuned dependencies; | changeset | files |
| Fri, 30 Jul 2004 10:44:27 +0200 | wenzelm | added context type solver; | changeset | files |
| Fri, 30 Jul 2004 10:42:19 +0200 | wenzelm | ZF/Simplifier: second copy of context type solver; | changeset | files |
| Fri, 30 Jul 2004 10:41:52 +0200 | wenzelm | tuned output; | changeset | files |
| Thu, 29 Jul 2004 17:45:21 +0200 | berghofe | - optimized nodup_vars check in capply | changeset | files |
| Thu, 29 Jul 2004 16:57:41 +0200 | paulson | removal of more iff-rules from RealDef.thy | changeset | files |
| Thu, 29 Jul 2004 16:14:42 +0200 | paulson | removed some [iff] declarations from RealDef.thy, concerning inequalities | changeset | files |
| Thu, 29 Jul 2004 16:14:06 +0200 | paulson | tidied | changeset | files |
| Thu, 29 Jul 2004 12:15:53 +0200 | paulson | documents for ZF-AC and ZF-Constructible | changeset | files |
| Wed, 28 Jul 2004 16:26:27 +0200 | paulson | conversion of SEQ.ML to Isar script | changeset | files |
| Wed, 28 Jul 2004 16:25:40 +0200 | paulson | abs notation | changeset | files |
| Wed, 28 Jul 2004 16:25:28 +0200 | paulson | fixed precedences | changeset | files |
| Wed, 28 Jul 2004 10:49:29 +0200 | paulson | conversion of Hyperreal/MacLaurin_lemmas to Isar script | changeset | files |
| Tue, 27 Jul 2004 15:39:59 +0200 | ballarin | *** empty log message *** | changeset | files |
| Mon, 26 Jul 2004 17:34:52 +0200 | paulson | converting Hyperreal/Transcendental to Isar script | changeset | files |
| Mon, 26 Jul 2004 15:48:50 +0200 | ballarin | New prover for transitive and reflexive-transitive closure of relations. | changeset | files |
| Thu, 22 Jul 2004 19:33:12 +0200 | webertj | minor formatting fixes | changeset | files |
| Thu, 22 Jul 2004 17:37:31 +0200 | nipkow | Modified \<Sum> syntax a little. | changeset | files |
| Thu, 22 Jul 2004 12:55:36 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 22 Jul 2004 10:33:26 +0200 | paulson | new material courtesy of Norbert Voelker | changeset | files |
| Wed, 21 Jul 2004 16:35:38 +0200 | wenzelm | updated; | changeset | files |
| Wed, 21 Jul 2004 08:35:29 +0200 | nipkow | Fixed latex problem | changeset | files |
| Tue, 20 Jul 2004 16:07:45 +0200 | nipkow | ring_1 -> ring | changeset | files |
| Tue, 20 Jul 2004 14:24:23 +0200 | paulson | minor tweaks to go with the new version of the Accountability paper | changeset | files |
| Tue, 20 Jul 2004 14:23:09 +0200 | paulson | removed some obsolete proofs | changeset | files |
| Tue, 20 Jul 2004 14:22:49 +0200 | paulson | two new results | changeset | files |
| Mon, 19 Jul 2004 18:21:26 +0200 | berghofe | Some changes to allow qualified theory import. | changeset | files |
| Mon, 19 Jul 2004 18:19:42 +0200 | berghofe | - Moved code generator setup for lists from Main.thy to List.thy | changeset | files |
| Mon, 19 Jul 2004 18:15:46 +0200 | berghofe | Moved code generator setup for lists to List.thy | changeset | files |
| Mon, 19 Jul 2004 18:14:57 +0200 | berghofe | Added function dest_list. | changeset | files |
| Mon, 19 Jul 2004 18:14:22 +0200 | berghofe | Added simple check that allows code generator to produce code containing | changeset | files |
| Mon, 19 Jul 2004 18:12:49 +0200 | berghofe | Added function unprefix. | changeset | files |
| Sun, 18 Jul 2004 12:01:08 +0200 | schirmer | tuned | changeset | files |
| Fri, 16 Jul 2004 19:21:59 +0200 | schirmer | added: get_extT_fields and | changeset | files |
| Fri, 16 Jul 2004 17:33:43 +0200 | nipkow | added Complex/root | changeset | files |
| Fri, 16 Jul 2004 17:33:12 +0200 | nipkow | Fine-tuned sum syntax. | changeset | files |
| Fri, 16 Jul 2004 17:32:34 +0200 | nipkow | Corrected TeX problem. | changeset | files |
| Fri, 16 Jul 2004 17:31:54 +0200 | nipkow | Created. | changeset | files |
| Fri, 16 Jul 2004 17:31:44 +0200 | nipkow | Corrected TeX problems. | changeset | files |
| Fri, 16 Jul 2004 11:46:59 +0200 | nipkow | Added nice latex syntax. | changeset | files |
| Fri, 16 Jul 2004 09:36:04 +0200 | wenzelm | int_ord = Int.compare, string_ord = String.compare; | changeset | files |
| Thu, 15 Jul 2004 15:47:39 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 15 Jul 2004 15:39:51 +0200 | nipkow | more summation syntax | changeset | files |
| Thu, 15 Jul 2004 15:39:40 +0200 | nipkow | more syntax | changeset | files |
| Thu, 15 Jul 2004 15:32:32 +0200 | paulson | redefining sumr to be a translation to setsum | changeset | files |
| Thu, 15 Jul 2004 13:24:45 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 15 Jul 2004 13:11:34 +0200 | nipkow | Moved to new m<..<n syntax for set intervals. | changeset | files |
| Thu, 15 Jul 2004 08:38:37 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 14 Jul 2004 10:25:21 +0200 | nipkow | ? | changeset | files |
| Wed, 14 Jul 2004 10:25:03 +0200 | nipkow | added {0::nat..n(} = {..n(} | changeset | files |
| Tue, 13 Jul 2004 12:32:01 +0200 | nipkow | Got rid of Summation and made it a translation into setsum instead. | changeset | files |
| Mon, 12 Jul 2004 19:56:58 +0200 | webertj | read_dimacs_cnf_file added | changeset | files |
| Mon, 12 Jul 2004 15:15:23 +0200 | oheimb | added README | changeset | files |
| Mon, 12 Jul 2004 15:05:30 +0200 | oheimb | corrected bibtex entry | changeset | files |
| Mon, 12 Jul 2004 12:11:46 +0200 | nipkow | *** empty log message *** | changeset | files |
| Sun, 11 Jul 2004 20:35:50 +0200 | wenzelm | context dependent components; | changeset | files |
| Sun, 11 Jul 2004 20:35:23 +0200 | wenzelm | added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b; | changeset | files |
| Sun, 11 Jul 2004 20:34:50 +0200 | wenzelm | improved print_ss; tuned; | changeset | files |
| Sun, 11 Jul 2004 20:34:25 +0200 | wenzelm | Simplifier and Classical Reasoner now support proof context dependent plug-ins; | changeset | files |
| Sun, 11 Jul 2004 20:33:22 +0200 | wenzelm | local_cla/simpset_of; | changeset | files |
| Fri, 09 Jul 2004 16:33:20 +0200 | berghofe | - Added support for conditional equations whose premises involve | changeset | files |
| Fri, 09 Jul 2004 16:29:10 +0200 | berghofe | - Expressed infer_derivs' in terms of infer_deriv | changeset | files |
| Fri, 09 Jul 2004 16:23:57 +0200 | berghofe | - Removed obsolete clause in function check_str | changeset | files |
| Fri, 09 Jul 2004 11:13:36 +0200 | paulson | new profiling function | changeset | files |
| Thu, 08 Jul 2004 19:34:56 +0200 | wenzelm | adapted type of simprocs; | changeset | files |
| Thu, 08 Jul 2004 19:34:18 +0200 | wenzelm | make SML/NJ happy; | changeset | files |
| Thu, 08 Jul 2004 19:34:10 +0200 | wenzelm | added add_term_varnames, term_varnames; | changeset | files |
| Thu, 08 Jul 2004 19:34:00 +0200 | wenzelm | got rid of obsolete meta_simpset; tuned; | changeset | files |
| Thu, 08 Jul 2004 19:33:51 +0200 | wenzelm | major cleanup; got rid of obsolete meta_simpset; | changeset | files |
| Thu, 08 Jul 2004 19:33:31 +0200 | wenzelm | tuned simprocs; | changeset | files |
| Thu, 08 Jul 2004 19:33:05 +0200 | wenzelm | got rid of obsolete meta_simpset; | changeset | files |
| Thu, 08 Jul 2004 19:32:53 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 08 Jul 2004 19:32:46 +0200 | wenzelm | removed obsolete dependency; | changeset | files |
| Tue, 06 Jul 2004 20:34:49 +0200 | schirmer | * Pure/Namespace: flag unique_names added | changeset | files |
| Tue, 06 Jul 2004 20:32:20 +0200 | schirmer | print_tac now outputs goals through trace-channel | changeset | files |
| Tue, 06 Jul 2004 20:31:37 +0200 | schirmer | added flag unique_names | changeset | files |
| Tue, 06 Jul 2004 20:31:06 +0200 | schirmer | * record_upd_simproc also simplifies trivial updates: | changeset | files |
| Sat, 03 Jul 2004 15:26:58 +0200 | berghofe | Added delete operation. | changeset | files |
| Thu, 01 Jul 2004 12:29:53 +0200 | paulson | new treatment of binary numerals | changeset | files |
| Wed, 30 Jun 2004 14:04:58 +0200 | schirmer | Added reference record_definition_quick_and_dirty_sensitive, to | changeset | files |
| Wed, 30 Jun 2004 00:42:59 +0200 | skalberg | Made simplification procedures simpset-aware. | changeset | files |
| Tue, 29 Jun 2004 11:18:34 +0200 | kleing | license change to BSD | changeset | files |
| Tue, 29 Jun 2004 10:07:56 +0200 | obua | support for sparse matrices | changeset | files |
| Mon, 28 Jun 2004 11:15:13 +0200 | paulson | new method for explicit classical resolution | changeset | files |
| Fri, 25 Jun 2004 15:03:05 +0200 | paulson | auto update | changeset | files |
| Fri, 25 Jun 2004 14:30:55 +0200 | skalberg | Merging the meta-simplifier with the Provers-simplifier. Next step: | changeset | files |
| Thu, 24 Jun 2004 17:54:53 +0200 | paulson | Norbert Voelker | changeset | files |
| Thu, 24 Jun 2004 17:52:55 +0200 | paulson | ringpower to recpower | changeset | files |
| Thu, 24 Jun 2004 17:52:02 +0200 | paulson | replaced monomorphic abs definitions by abs_if | changeset | files |
| Thu, 24 Jun 2004 17:51:28 +0200 | paulson | tidied | changeset | files |
| Wed, 23 Jun 2004 14:44:22 +0200 | skalberg | Moved conversion rules from MetaSimplifier to Drule. refl_implies removed | changeset | files |
| Wed, 23 Jun 2004 09:09:18 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 22 Jun 2004 14:14:08 +0200 | webertj | faster conversion into DIMACS CNF and DIMACS SAT format | changeset | files |
| Tue, 22 Jun 2004 10:05:47 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 22 Jun 2004 09:52:15 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 22 Jun 2004 09:52:08 +0200 | wenzelm | improved print_theory; | changeset | files |
| Tue, 22 Jun 2004 09:51:59 +0200 | wenzelm | added output, removed pp_undef; | changeset | files |
| Tue, 22 Jun 2004 09:51:51 +0200 | wenzelm | added chars_only, symbol_output; | changeset | files |
| Tue, 22 Jun 2004 09:51:39 +0200 | wenzelm | tuned certify_typ/term; | changeset | files |
| Tue, 22 Jun 2004 09:51:23 +0200 | wenzelm | tuned output; | changeset | files |
| Mon, 21 Jun 2004 16:49:58 +0200 | wenzelm | added unparse; | changeset | files |
| Mon, 21 Jun 2004 16:41:06 +0200 | wenzelm | pretty_abbr; | changeset | files |
| Mon, 21 Jun 2004 16:40:55 +0200 | wenzelm | tuned certify_typ; | changeset | files |
| Mon, 21 Jun 2004 16:40:44 +0200 | wenzelm | Type.cert_typ; | changeset | files |
| Mon, 21 Jun 2004 16:40:30 +0200 | wenzelm | tuned certify_term; | changeset | files |
| Mon, 21 Jun 2004 16:40:08 +0200 | wenzelm | added certify_class/sort; | changeset | files |
| Mon, 21 Jun 2004 16:39:58 +0200 | wenzelm | added >>> : transition list -> unit; | changeset | files |
| Mon, 21 Jun 2004 16:39:39 +0200 | wenzelm | immediate_output; | changeset | files |
| Mon, 21 Jun 2004 16:39:18 +0200 | wenzelm | avoid \...\; | changeset | files |
| Mon, 21 Jun 2004 16:39:09 +0200 | wenzelm | File.quote_sysify_path; | changeset | files |
| Mon, 21 Jun 2004 10:25:57 +0200 | kleing | Merged in license change from Isabelle2004 | changeset | files |
| Sun, 20 Jun 2004 09:30:12 +0200 | wenzelm | got rid of Output.output for default print mode; | changeset | files |
| Sun, 20 Jun 2004 09:28:35 +0200 | wenzelm | added checkTimer; | changeset | files |
| Sun, 20 Jun 2004 09:27:40 +0200 | wenzelm | added accumulated timing; | changeset | files |
| Sun, 20 Jun 2004 09:27:32 +0200 | wenzelm | added escape, export encode_raw, default mode now trivial, tuned; | changeset | files |
| Sun, 20 Jun 2004 09:27:24 +0200 | wenzelm | use_output: Symbol.escape; | changeset | files |
| Sun, 20 Jun 2004 09:27:17 +0200 | wenzelm | tuned pp; | changeset | files |
| Sun, 20 Jun 2004 09:27:04 +0200 | wenzelm | avoid premature evaluation of syn_of (wastes time in conjunction with pp); | changeset | files |
| Sun, 20 Jun 2004 09:26:48 +0200 | wenzelm | Symbol.encode_raw; | changeset | files |
| Sun, 20 Jun 2004 09:26:29 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 18 Jun 2004 20:10:52 +0200 | wenzelm | improved comments -- required by 'isatool latex -o syms'; | changeset | files |
| Fri, 18 Jun 2004 20:07:59 +0200 | wenzelm | more generous treatment of packages in draft prints; | changeset | files |
| Fri, 18 Jun 2004 20:07:51 +0200 | wenzelm | scalable string_of_tree; tuned; | changeset | files |
| Fri, 18 Jun 2004 20:07:42 +0200 | wenzelm | tuned exists_string; | changeset | files |
| Fri, 18 Jun 2004 20:07:31 +0200 | wenzelm | isatool_document: verbose option; | changeset | files |
| Fri, 18 Jun 2004 00:32:54 +0200 | aspinall | Add \usepackage{latexsym} | changeset | files |
| Thu, 17 Jun 2004 22:01:23 +0200 | webertj | new SAT solver interface | changeset | files |
| Thu, 17 Jun 2004 21:58:51 +0200 | webertj | improved defcnf conversion | changeset | files |
| Thu, 17 Jun 2004 17:18:30 +0200 | paulson | removal of magmas and semigroups | changeset | files |
| Thu, 17 Jun 2004 14:27:01 +0200 | wenzelm | fixed 'requires' comments, which are needed for printing of drafts; | changeset | files |
| Thu, 17 Jun 2004 14:26:43 +0200 | wenzelm | isub/isup quasi letter (again); tuned; | changeset | files |
| Thu, 17 Jun 2004 14:26:24 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 17 Jun 2004 14:24:43 +0200 | schirmer | tuned | changeset | files |
| Wed, 16 Jun 2004 20:42:22 +0200 | wenzelm | isatool_document: writeln output; | changeset | files |
| Wed, 16 Jun 2004 20:37:29 +0200 | wenzelm | tuned document; | changeset | files |
| Wed, 16 Jun 2004 20:37:14 +0200 | wenzelm | prevent looping of error messages involving malformed symbols; | changeset | files |
| Wed, 16 Jun 2004 20:37:00 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 16 Jun 2004 20:36:43 +0200 | wenzelm | removed unused help function; | changeset | files |
| Wed, 16 Jun 2004 14:56:58 +0200 | paulson | new fib example | changeset | files |
| Wed, 16 Jun 2004 14:56:39 +0200 | paulson | removal of x-symbol syntax <Sigma> for dependent products | changeset | files |
| Tue, 15 Jun 2004 13:24:19 +0200 | wenzelm | ISABELLE_TMP | changeset | files |
| Tue, 15 Jun 2004 13:24:02 +0200 | wenzelm | path instead of string; | changeset | files |
| Tue, 15 Jun 2004 13:23:39 +0200 | wenzelm | added path; | changeset | files |
| Tue, 15 Jun 2004 13:23:23 +0200 | wenzelm | tuned lexical syntax; | changeset | files |
| Tue, 15 Jun 2004 13:22:56 +0200 | wenzelm | num tokens; | changeset | files |
| Tue, 15 Jun 2004 10:47:08 +0200 | paulson | fixed bad link | changeset | files |
| Tue, 15 Jun 2004 10:46:33 +0200 | paulson | slight speed improvement | changeset | files |
| Tue, 15 Jun 2004 10:40:05 +0200 | paulson | strengthened some theorems | changeset | files |
| Tue, 15 Jun 2004 00:50:10 +0200 | webertj | Jerusat settings added | changeset | files |
| Tue, 15 Jun 2004 00:06:40 +0200 | webertj | entries for ZChaff and BerkMin added/modified | changeset | files |
| Mon, 14 Jun 2004 16:46:48 +0200 | chaieb | Oracle corrected | changeset | files |
| Mon, 14 Jun 2004 14:20:55 +0200 | obua | Further development of matrix theory | changeset | files |
| Sun, 13 Jun 2004 17:57:35 +0200 | webertj | faster defcnf conversion | changeset | files |
| Sun, 13 Jun 2004 15:43:55 +0200 | wenzelm | updated; | changeset | files |
| Sun, 13 Jun 2004 15:31:21 +0200 | wenzelm | updated; | changeset | files |
| Sun, 13 Jun 2004 15:31:11 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 13 Jun 2004 15:30:58 +0200 | wenzelm | tuned Present.drafts; | changeset | files |
| Sun, 13 Jun 2004 15:30:08 +0200 | wenzelm | added display_drafts and print_drafts commands; | changeset | files |
| Sun, 13 Jun 2004 15:28:46 +0200 | wenzelm | added PRINT_COMMAND setting | changeset | files |
| Sun, 13 Jun 2004 15:28:30 +0200 | wenzelm | added isatool display and isatool print; | changeset | files |
| Sun, 13 Jun 2004 15:28:19 +0200 | wenzelm | print document | changeset | files |
| Sun, 13 Jun 2004 15:28:12 +0200 | wenzelm | display document (in DVI format) | changeset | files |
| Sat, 12 Jun 2004 22:47:35 +0200 | wenzelm | root for draft documents; | changeset | files |
| Sat, 12 Jun 2004 22:46:51 +0200 | wenzelm | Library.translate_string; | changeset | files |
| Sat, 12 Jun 2004 22:46:39 +0200 | wenzelm | added trace (inefficient for very long input); | changeset | files |
| Sat, 12 Jun 2004 22:46:21 +0200 | wenzelm | added translate_string; | changeset | files |
| Sat, 12 Jun 2004 22:45:59 +0200 | wenzelm | added read (provides transition names and sources); | changeset | files |
| Sat, 12 Jun 2004 22:45:46 +0200 | wenzelm | added output_known_symbols; tuned; | changeset | files |
| Sat, 12 Jun 2004 22:45:35 +0200 | wenzelm | added name_of, source_of, source; | changeset | files |
| Sat, 12 Jun 2004 22:45:18 +0200 | wenzelm | added Present.drafts; | changeset | files |
| Sat, 12 Jun 2004 22:44:58 +0200 | wenzelm | added option 'isatool latex -o syms'; | changeset | files |
| Sat, 12 Jun 2004 13:50:55 +0200 | chaieb | An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on. | changeset | files |
| Thu, 10 Jun 2004 20:17:07 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 10 Jun 2004 20:12:49 +0200 | wenzelm | improved RemoteFile; | changeset | files |
| Thu, 10 Jun 2004 20:11:51 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 10 Jun 2004 18:46:35 +0200 | aspinall | Removed this: not really ready yet. | changeset | files |
| Thu, 10 Jun 2004 18:41:47 +0200 | aspinall | Interface configuration for Isar | changeset | files |
| Wed, 09 Jun 2004 20:24:32 +0200 | wenzelm | Sign.is_logtype; | changeset | files |
| Wed, 09 Jun 2004 18:57:18 +0200 | wenzelm | prs: Output.output; | changeset | files |
| Wed, 09 Jun 2004 18:56:55 +0200 | wenzelm | added split_ext; removed drop_ext; | changeset | files |
| Wed, 09 Jun 2004 18:56:47 +0200 | wenzelm | tuned comment; | changeset | files |
| Wed, 09 Jun 2004 18:56:38 +0200 | wenzelm | Scan.this_string; | changeset | files |
| Wed, 09 Jun 2004 18:56:30 +0200 | wenzelm | tuned representation; added RemoteFile; | changeset | files |
| Wed, 09 Jun 2004 18:56:21 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 09 Jun 2004 18:56:09 +0200 | wenzelm | added this_string; | changeset | files |
| Wed, 09 Jun 2004 18:55:28 +0200 | wenzelm | tuned messages; | changeset | files |
| Wed, 09 Jun 2004 18:55:07 +0200 | wenzelm | added is_logtype (replaces logtypes field of syntax); tuned merge; | changeset | files |
| Wed, 09 Jun 2004 18:54:43 +0200 | wenzelm | removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode; | changeset | files |
| Wed, 09 Jun 2004 18:54:26 +0200 | wenzelm | removed separate logtypes field of syntax; | changeset | files |
| Wed, 09 Jun 2004 18:54:07 +0200 | wenzelm | Path.split_ext; more robust inform_file_processed; | changeset | files |
| Wed, 09 Jun 2004 18:53:41 +0200 | wenzelm | Sign.is_logtype; | changeset | files |
| Wed, 09 Jun 2004 18:53:13 +0200 | wenzelm | Syntax.default_mode; | changeset | files |
| Wed, 09 Jun 2004 18:52:55 +0200 | wenzelm | added option 'locale=NAME'; | changeset | files |
| Wed, 09 Jun 2004 18:52:42 +0200 | wenzelm | Url.File; | changeset | files |
| Wed, 09 Jun 2004 18:52:11 +0200 | wenzelm | * Document preparation: antiquotations provide option 'locale=NAME'; | changeset | files |
| Wed, 09 Jun 2004 18:51:26 +0200 | wenzelm | tuned comment; | changeset | files |
| Wed, 09 Jun 2004 18:51:16 +0200 | wenzelm | updated/tuned identifier syntax; | changeset | files |
| Wed, 09 Jun 2004 18:51:02 +0200 | wenzelm | updated notes on sub-/superscripts; | changeset | files |
| Wed, 09 Jun 2004 18:50:38 +0200 | wenzelm | removed Syntax.test_read; | changeset | files |
| Wed, 09 Jun 2004 15:00:32 +0200 | nipkow | added a lemma lfp_ordinal_induct | changeset | files |
| Wed, 09 Jun 2004 12:24:02 +0200 | paulson | fixed the groupI ambiguity | changeset | files |