| Fri, 05 May 2000 21:58:44 +0200 | wenzelm | GPLed; | changeset | files |
| Fri, 05 May 2000 21:58:18 +0200 | wenzelm | added simple_read_term; | changeset | files |
| Fri, 05 May 2000 21:57:58 +0200 | wenzelm | tuned msg; | changeset | files |
| Fri, 05 May 2000 18:24:06 +0200 | nipkow | Added constant abs. | changeset | files |
| Fri, 05 May 2000 17:49:54 +0200 | paulson | simprocs now simplify the RHS of their result | changeset | files |
| Fri, 05 May 2000 17:49:34 +0200 | paulson | new lemmas about binary division | changeset | files |
| Fri, 05 May 2000 12:51:33 +0200 | nipkow | Added AVL | changeset | files |
| Thu, 04 May 2000 18:40:57 +0200 | paulson | if_weak_cong should make linear arithmetic faster | changeset | files |
| Thu, 04 May 2000 18:39:51 +0200 | paulson | a safer way of proving literal equalities | changeset | files |
| Thu, 04 May 2000 15:17:41 +0200 | paulson | from Suc...Suc to #m | changeset | files |
| Thu, 04 May 2000 15:16:46 +0200 | paulson | of course it should use Main | changeset | files |
| Thu, 04 May 2000 15:16:18 +0200 | paulson | new lemmas concerning powers and #mmm | changeset | files |
| Thu, 04 May 2000 15:15:37 +0200 | paulson | changed 2 to #2 | changeset | files |
| Thu, 04 May 2000 15:14:56 +0200 | paulson | Suc 0 -> 1 | changeset | files |
| Thu, 04 May 2000 15:14:44 +0200 | paulson | card_Pow is no longer a default simprule because it uses unary 2 | changeset | files |
| Thu, 04 May 2000 12:29:18 +0200 | paulson | simprocs | changeset | files |
| Thu, 04 May 2000 12:29:00 +0200 | paulson | further tidying of integer simprocs | changeset | files |
| Wed, 03 May 2000 18:34:09 +0200 | paulson | removed obsolete simproc combine_coeff | changeset | files |
| Wed, 03 May 2000 18:33:28 +0200 | paulson | Installation of CombineNumerals for the integers | changeset | files |
| Wed, 03 May 2000 18:30:29 +0200 | paulson | removed obsolete simprocs | changeset | files |
| Tue, 02 May 2000 18:56:39 +0200 | paulson | removed obsolete "evenness" proofs | changeset | files |
| Tue, 02 May 2000 18:55:33 +0200 | paulson | TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES | changeset | files |
| Tue, 02 May 2000 18:55:11 +0200 | paulson | modified for new simprocs | changeset | files |
| Tue, 02 May 2000 18:54:59 +0200 | paulson | now using binary naturals | changeset | files |
| Tue, 02 May 2000 18:54:38 +0200 | paulson | various bug fixes | changeset | files |
| Tue, 02 May 2000 18:45:17 +0200 | paulson | Cassini identity is easier to prove using INTEGERS | changeset | files |
| Tue, 02 May 2000 18:44:33 +0200 | paulson | a more modern proof | changeset | files |
| Tue, 02 May 2000 18:42:48 +0200 | paulson | now with combine_numerals | changeset | files |
| Tue, 02 May 2000 18:40:16 +0200 | paulson | combine_numerals replaces both fold_Suc and combine_coeff | changeset | files |
| Tue, 02 May 2000 18:39:34 +0200 | paulson | new simproc, replacing combine_coeffs and working for nat, int, real | changeset | files |
| Fri, 28 Apr 2000 10:44:20 +0200 | paulson | signature change | changeset | files |
| Fri, 28 Apr 2000 10:44:03 +0200 | paulson | inserted triviality check | changeset | files |
| Tue, 25 Apr 2000 08:09:10 +0200 | nipkow | *** empty log message *** | changeset | files |
| Sun, 23 Apr 2000 11:41:45 +0200 | paulson | new, but still slow, proofs using binary numerals | changeset | files |
| Sun, 23 Apr 2000 11:41:06 +0200 | paulson | [Int_CC.sum_conv, Int_CC.rel_conv] no longer exist | changeset | files |
| Sun, 23 Apr 2000 11:39:56 +0200 | paulson | number_of now takes a type arg | changeset | files |
| Sun, 23 Apr 2000 11:39:32 +0200 | paulson | this change saves 15 seconds | changeset | files |
| Sun, 23 Apr 2000 11:35:00 +0200 | paulson | bug fixes to new simprocs | changeset | files |
| Sun, 23 Apr 2000 11:34:41 +0200 | paulson | [Int_CC.sum_conv, Int_CC.rel_conv] no longer exist | changeset | files |
| Sun, 23 Apr 2000 11:34:05 +0200 | paulson | removed some duplication, etc. | changeset | files |
| Sun, 23 Apr 2000 11:33:41 +0200 | paulson | now uses the new cancel_numerals simproc | changeset | files |
| Fri, 21 Apr 2000 11:36:00 +0200 | paulson | Provers/Arith/inverse_fold.ML is already obsolete | changeset | files |
| Fri, 21 Apr 2000 11:31:38 +0200 | paulson | cleaner exceptions | changeset | files |
| Fri, 21 Apr 2000 11:31:03 +0200 | paulson | now works for coefficients, not just for numerals | changeset | files |
| Fri, 21 Apr 2000 11:29:57 +0200 | paulson | new file containing simproc invocations, from NatBin.ML | changeset | files |
| Fri, 21 Apr 2000 11:29:33 +0200 | paulson | moved the simproc code to NatSimprocs.ML | changeset | files |
| Fri, 21 Apr 2000 11:28:34 +0200 | paulson | Provers/Arith/inverse_fold.ML is already obsolete | changeset | files |
| Fri, 21 Apr 2000 11:28:18 +0200 | paulson | new file Integ/NatSimprocs.ML | changeset | files |
| Fri, 21 Apr 2000 11:27:28 +0200 | paulson | Provers/Arith/inverse_fold.ML is already obsolete | changeset | files |
| Thu, 20 Apr 2000 09:54:56 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 19 Apr 2000 15:27:08 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 19 Apr 2000 14:22:11 +0200 | wenzelm | TuturialI; | changeset | files |
| Wed, 19 Apr 2000 13:40:42 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 19 Apr 2000 13:20:16 +0200 | wenzelm | check_file: keep expanded (!) absolute path; | changeset | files |
| Wed, 19 Apr 2000 12:59:38 +0200 | nipkow | Adding generated files | changeset | files |
| Wed, 19 Apr 2000 12:59:21 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 19 Apr 2000 12:56:24 +0200 | wenzelm | fixed -c default value; | changeset | files |
| Wed, 19 Apr 2000 12:54:56 +0200 | nipkow | Adding generated files. | changeset | files |
| Wed, 19 Apr 2000 11:56:31 +0200 | nipkow | I wonder which files i forgot. | changeset | files |
| Wed, 19 Apr 2000 11:56:06 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 19 Apr 2000 11:54:39 +0200 | nipkow | I wonder if that's all? | changeset | files |
| Wed, 19 Apr 2000 11:13:31 +0200 | paulson | deleted obsolete lemma_not_leI2 | changeset | files |
| Wed, 19 Apr 2000 11:09:59 +0200 | paulson | removal of less_SucI, le_SucI from default simpset | changeset | files |
| Tue, 18 Apr 2000 15:56:41 +0200 | paulson | replaced obsolete diff_right_cancel by diff_diff_eq | changeset | files |
| Tue, 18 Apr 2000 15:54:56 +0200 | paulson | added number_of_const: term | changeset | files |
| Tue, 18 Apr 2000 15:54:31 +0200 | paulson | tidied | changeset | files |
| Tue, 18 Apr 2000 15:53:50 +0200 | paulson | instantiates new simprocs for numerals of type "nat" | changeset | files |
| Tue, 18 Apr 2000 15:51:59 +0200 | paulson | new simprocs for numerals of type "nat" | changeset | files |
| Tue, 18 Apr 2000 14:57:18 +0200 | wenzelm | emilimated global names; | changeset | files |
| Tue, 18 Apr 2000 14:54:08 +0200 | wenzelm | removed obsolete "simpset" keyword; | changeset | files |
| Tue, 18 Apr 2000 00:49:49 +0200 | wenzelm | renamed 'hide' to 'hide_action'; | changeset | files |
| Tue, 18 Apr 2000 00:36:02 +0200 | wenzelm | fixed theory deps; | changeset | files |
| Mon, 17 Apr 2000 14:27:10 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Mon, 17 Apr 2000 14:20:41 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Mon, 17 Apr 2000 14:12:33 +0200 | wenzelm | * improved name spaces: ambiguous output is qualified; support for | changeset | files |
| Mon, 17 Apr 2000 14:10:38 +0200 | wenzelm | improved output of ambiguous entries; | changeset | files |
| Mon, 17 Apr 2000 14:10:04 +0200 | wenzelm | Pretty.chunks; | changeset | files |
| Mon, 17 Apr 2000 14:08:51 +0200 | wenzelm | 'global' / 'local': comment; | changeset | files |
| Mon, 17 Apr 2000 14:08:19 +0200 | wenzelm | name space hide operations; | changeset | files |
| Mon, 17 Apr 2000 14:07:00 +0200 | wenzelm | global/local_path: comment; | changeset | files |
| Mon, 17 Apr 2000 14:06:05 +0200 | wenzelm | added 'hide'; | changeset | files |
| Mon, 17 Apr 2000 14:04:46 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 17 Apr 2000 14:03:51 +0200 | wenzelm | NameSpace.is_qualified; | changeset | files |
| Mon, 17 Apr 2000 13:57:55 +0200 | wenzelm | Pretty.chunks; | changeset | files |
| Sat, 15 Apr 2000 17:41:20 +0200 | nipkow | mod to error msg | changeset | files |
| Sat, 15 Apr 2000 15:01:31 +0200 | wenzelm | next_block: reset_facts; | changeset | files |
| Sat, 15 Apr 2000 15:00:57 +0200 | wenzelm | plain ASCII; | changeset | files |
| Fri, 14 Apr 2000 17:30:22 +0200 | wenzelm | intrn_arity: reject type abbreviations; | changeset | files |
| Fri, 14 Apr 2000 17:29:57 +0200 | wenzelm | added is_type_abbr; | changeset | files |
| Fri, 14 Apr 2000 16:12:46 +0200 | wenzelm | \newenvironment{isabellequote}; | changeset | files |
| Fri, 14 Apr 2000 15:55:40 +0200 | wenzelm | global \isa@parindent, \isa@parskip; | changeset | files |
| Fri, 14 Apr 2000 01:14:51 +0200 | wenzelm | use HOLogic.termT; | changeset | files |
| Thu, 13 Apr 2000 17:49:42 +0200 | wenzelm | outer syntax: no simps; | changeset | files |
| Thu, 13 Apr 2000 17:49:08 +0200 | wenzelm | recdef: no simps; | changeset | files |
| Thu, 13 Apr 2000 15:19:37 +0200 | paulson | stopped using the obsolete "nat_ind_tac" | changeset | files |
| Thu, 13 Apr 2000 15:18:02 +0200 | paulson | added some new iff-lemmas; removed some obsolete thms | changeset | files |
| Thu, 13 Apr 2000 15:16:32 +0200 | paulson | tidied | changeset | files |
| Thu, 13 Apr 2000 15:11:41 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 13 Apr 2000 15:02:57 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 13 Apr 2000 15:02:02 +0200 | wenzelm | Simplifier options; | changeset | files |
| Thu, 13 Apr 2000 15:01:50 +0200 | nipkow | Times -> <*> | changeset | files |
| Thu, 13 Apr 2000 15:01:45 +0200 | wenzelm | fixed ??/?; | changeset | files |
| Thu, 13 Apr 2000 15:01:35 +0200 | wenzelm | fixed index; | changeset | files |
| Thu, 13 Apr 2000 15:01:11 +0200 | wenzelm | added simp_options; | changeset | files |
| Thu, 13 Apr 2000 15:00:42 +0200 | wenzelm | intro/elim_tac: match only; | changeset | files |
| Thu, 13 Apr 2000 10:30:28 +0200 | nipkow | made mod_less_divisor a simplification rule. | changeset | files |
| Wed, 12 Apr 2000 23:52:50 +0200 | wenzelm | InductMethod.concls_of; | changeset | files |
| Wed, 12 Apr 2000 23:52:21 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 12 Apr 2000 23:51:57 +0200 | wenzelm | export concl_of; | changeset | files |
| Wed, 12 Apr 2000 23:49:10 +0200 | wenzelm | tuned \isasymlbrace; | changeset | files |
| Wed, 12 Apr 2000 23:47:47 +0200 | wenzelm | 'insts' syntax; | changeset | files |
| Wed, 12 Apr 2000 23:46:06 +0200 | wenzelm | improved 'induct(_tac)' syntax; | changeset | files |
| Wed, 12 Apr 2000 23:45:21 +0200 | wenzelm | added 'insert' method; | changeset | files |
| Wed, 12 Apr 2000 23:45:01 +0200 | wenzelm | added inst, insts; | changeset | files |
| Wed, 12 Apr 2000 18:53:20 +0200 | wenzelm | improved induct_tac; | changeset | files |
| Wed, 12 Apr 2000 18:53:09 +0200 | wenzelm | induct stripped: match_tac; | changeset | files |
| Wed, 12 Apr 2000 18:47:03 +0200 | wenzelm | Args.name_dummy; | changeset | files |
| Wed, 12 Apr 2000 15:40:19 +0200 | wenzelm | fixed 'induct_tac' syntax; | changeset | files |
| Mon, 10 Apr 2000 23:38:02 +0200 | wenzelm | handle dir prefix; | changeset | files |
| Mon, 10 Apr 2000 23:36:19 +0200 | wenzelm | improved document preparation; | changeset | files |