| Sun, 21 May 2000 21:49:06 +0200 | wenzelm | added notes; | changeset | files |
| Sun, 21 May 2000 21:48:39 +0200 | wenzelm | new Isar version; | changeset | files |
| Sun, 21 May 2000 14:49:28 +0200 | wenzelm | replaced {{ }} by { }; | changeset | files |
| Sun, 21 May 2000 14:44:01 +0200 | wenzelm | cite isabelle-axclass; | changeset | files |
| Sun, 21 May 2000 14:42:35 +0200 | wenzelm | improved \BG, \EN; | changeset | files |
| Sun, 21 May 2000 14:37:17 +0200 | wenzelm | removed is_type_abbr; | changeset | files |
| Sun, 21 May 2000 14:36:29 +0200 | wenzelm | removed is_type_abbr; | changeset | files |
| Sun, 21 May 2000 14:35:27 +0200 | wenzelm | adapted to inner syntax of sorts; | changeset | files |
| Sun, 21 May 2000 14:33:46 +0200 | wenzelm | replaced {{ }} by { }; | changeset | files |
| Sun, 21 May 2000 14:32:47 +0200 | wenzelm | added sort_of_term; | changeset | files |
| Sun, 21 May 2000 14:31:41 +0200 | wenzelm | added read_sort; | changeset | files |
| Sun, 21 May 2000 01:18:29 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Sun, 21 May 2000 01:17:12 +0200 | wenzelm | new stuff; | changeset | files |
| Sun, 21 May 2000 01:16:54 +0200 | wenzelm | \urlstyle{rm}; | changeset | files |
| Sun, 21 May 2000 01:12:00 +0200 | wenzelm | snapshot of new Isar'ized version; | changeset | files |
| Sat, 20 May 2000 18:37:21 +0200 | nipkow | added lemma. | changeset | files |
| Sat, 20 May 2000 15:15:02 +0200 | nipkow | fixed link | changeset | files |
| Thu, 18 May 2000 19:10:08 +0200 | wenzelm | * HOL/ML: even fewer consts are declared as global (see theories Ord, | changeset | files |
| Thu, 18 May 2000 19:04:04 +0200 | wenzelm | print_state: flag for proof only; | changeset | files |
| Thu, 18 May 2000 18:48:55 +0200 | wenzelm | hide: check declared; | changeset | files |
| Thu, 18 May 2000 18:46:13 +0200 | wenzelm | added disable_pr, enable_pr; | changeset | files |
| Thu, 18 May 2000 17:21:58 +0200 | wenzelm | 'pr' now prints actual proof states only; | changeset | files |
| Thu, 18 May 2000 11:43:57 +0200 | wenzelm | fewer consts declared as global; | changeset | files |
| Thu, 18 May 2000 11:40:57 +0200 | wenzelm | 'apply' consumes facts; | changeset | files |
| Wed, 17 May 2000 18:27:13 +0200 | wenzelm | Proof General -- if present make this the default; | changeset | files |
| Wed, 17 May 2000 17:16:21 +0200 | wenzelm | export generic_simp_tac; | changeset | files |
| Tue, 16 May 2000 14:07:49 +0200 | paulson | changed to cope with the rewriting of #2+n to Suc(Suc n) | changeset | files |
| Tue, 16 May 2000 14:07:06 +0200 | paulson | new policy to simplify the use of numerals: | changeset | files |
| Tue, 16 May 2000 14:04:29 +0200 | paulson | reverted to old proof of dominoes_tile_row, given new treatment of #2+... | changeset | files |
| Mon, 15 May 2000 17:34:05 +0200 | berghofe | Replaced some definitions involving epsilon by more readable primrec | changeset | files |
| Mon, 15 May 2000 17:32:39 +0200 | berghofe | alist_rec and assoc are now defined using primrec and thus no longer | changeset | files |
| Mon, 15 May 2000 17:30:19 +0200 | berghofe | Removed unnecessary primrec equations of hd and last involving arbitrary. | changeset | files |
| Mon, 15 May 2000 10:34:51 +0200 | paulson | collected three proofs into rename_client_map_tac | changeset | files |
| Mon, 15 May 2000 10:33:32 +0200 | paulson | added the dummy theory Integ/NatSimprocs.thy | changeset | files |
| Fri, 12 May 2000 15:21:58 +0200 | paulson | updated | changeset | files |
| Fri, 12 May 2000 15:20:46 +0200 | paulson | new simprules needed because of new subtraction rewriting | changeset | files |
| Fri, 12 May 2000 15:18:55 +0200 | paulson | nat_diff_split' now called nat_diff_split | changeset | files |
| Fri, 12 May 2000 15:15:27 +0200 | paulson | deleted a lot of obsolete arithmetic lemmas | changeset | files |
| Fri, 12 May 2000 15:14:35 +0200 | paulson | tidied | changeset | files |
| Fri, 12 May 2000 15:14:08 +0200 | paulson | new simprules for nat_case and nat_rec | changeset | files |
| Fri, 12 May 2000 15:11:42 +0200 | paulson | tidying, especially to remove zcompare_rls from proofs | changeset | files |
| Fri, 12 May 2000 15:06:35 +0200 | paulson | a massive tidy-up | changeset | files |
| Fri, 12 May 2000 15:05:02 +0200 | paulson | NatSimprocs is now a theory, not a file | changeset | files |
| Fri, 12 May 2000 15:02:57 +0200 | paulson | new theorem one_le_power | changeset | files |
| Fri, 12 May 2000 15:00:45 +0200 | paulson | tidied | changeset | files |
| Fri, 12 May 2000 14:59:12 +0200 | paulson | deleted some redundant simprules | changeset | files |
| Fri, 12 May 2000 14:57:28 +0200 | paulson | new dummy theory; prevents strange errors when loading NatSimprocs.ML | changeset | files |
| Fri, 12 May 2000 11:52:44 +0200 | wenzelm | improved name of simproc; | changeset | files |
| Wed, 10 May 2000 22:34:30 +0200 | wenzelm | fixed theory deps; | changeset | files |
| Wed, 10 May 2000 21:04:16 +0200 | wenzelm | base on IntArith instead of Int (in order to leave out deleted simproc!); | changeset | files |
| Wed, 10 May 2000 21:03:12 +0200 | wenzelm | dest_mss: sort procs wrt. names; | changeset | files |
| Wed, 10 May 2000 16:43:39 +0200 | wenzelm | FAKE_BUILD; | changeset | files |
| Wed, 10 May 2000 16:43:25 +0200 | wenzelm | polyml; | changeset | files |
| Wed, 10 May 2000 16:43:10 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 10 May 2000 13:36:27 +0200 | paulson | new default simprule for better compatibility with old setup | changeset | files |
| Wed, 10 May 2000 11:17:01 +0200 | paulson | tidied | changeset | files |
| Wed, 10 May 2000 01:13:43 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 09 May 2000 16:05:45 +0200 | wenzelm | use proper version of pdfsetup.sty; | changeset | files |
| Tue, 09 May 2000 16:05:30 +0200 | wenzelm | added semicolons; | changeset | files |
| Tue, 09 May 2000 15:10:25 +0200 | wenzelm | updated keywords; | changeset | files |
| Tue, 09 May 2000 14:33:43 +0200 | wenzelm | named "op ^" definitions; | changeset | files |
| Tue, 09 May 2000 14:16:32 +0200 | wenzelm | improved X-Symbol stuff; | changeset | files |
| Tue, 09 May 2000 11:29:13 +0200 | paulson | more examples | changeset | files |
| Mon, 08 May 2000 21:00:27 +0200 | wenzelm | added INSTALL; | changeset | files |
| Mon, 08 May 2000 20:59:30 +0200 | wenzelm | moved theory Sexp to Induct examples; | changeset | files |
| Mon, 08 May 2000 20:58:49 +0200 | wenzelm | strip = impI allI allI; | changeset | files |
| Mon, 08 May 2000 20:57:02 +0200 | wenzelm | replaced rabs by overloaded abs; | changeset | files |
| Mon, 08 May 2000 18:20:04 +0200 | paulson | yet another example | changeset | files |
| Mon, 08 May 2000 16:59:18 +0200 | paulson | new example | changeset | files |
| Mon, 08 May 2000 16:59:02 +0200 | paulson | tidied | changeset | files |
| Mon, 08 May 2000 16:58:44 +0200 | paulson | better simplification of the result of simprocs | changeset | files |
| Mon, 08 May 2000 16:58:18 +0200 | paulson | moved le_square, proved le_cube | changeset | files |
| Mon, 08 May 2000 16:57:53 +0200 | paulson | more details | changeset | files |
| Mon, 08 May 2000 11:45:57 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 08 May 2000 11:45:47 +0200 | wenzelm | val needs_filtered_use = true; | changeset | files |
| Mon, 08 May 2000 11:35:19 +0200 | wenzelm | recovered \seealso; | changeset | files |
| Mon, 08 May 2000 11:13:28 +0200 | wenzelm | improved indexing; | changeset | files |
| Mon, 08 May 2000 11:13:11 +0200 | wenzelm | \usepackage{makeidx}; | changeset | files |
| Mon, 08 May 2000 11:03:53 +0200 | wenzelm | tuned GARBAGE; | changeset | files |
| Mon, 08 May 2000 10:53:13 +0200 | wenzelm | improved handling of Isabelle styles (less garbage); | changeset | files |
| Mon, 08 May 2000 10:52:46 +0200 | wenzelm | updated; | changeset | files |
| Mon, 08 May 2000 10:52:28 +0200 | wenzelm | updated syntax of simp options: (no_asm) etc.; | changeset | files |
| Mon, 08 May 2000 10:51:07 +0200 | wenzelm | removed \isabelledefaultstyle (use \isabellestyle instead); | changeset | files |
| Mon, 08 May 2000 10:49:27 +0200 | wenzelm | always discgarb -c; | changeset | files |
| Sat, 06 May 2000 00:46:13 +0200 | wenzelm | fixed clash with new 'abs' const; | changeset | files |
| Fri, 05 May 2000 22:37:04 +0200 | wenzelm | use Sign.simple_read_term; | changeset | files |
| Fri, 05 May 2000 22:35:51 +0200 | wenzelm | error msg: counting from one (again), in order to be consistent with | changeset | files |
| Fri, 05 May 2000 22:34:40 +0200 | wenzelm | tuned messages; | changeset | files |
| Fri, 05 May 2000 22:32:49 +0200 | wenzelm | removed dead code: listof; | changeset | files |
| Fri, 05 May 2000 22:32:25 +0200 | wenzelm | use Args.colon / Args.parens; | changeset | files |
| Fri, 05 May 2000 22:30:14 +0200 | wenzelm | adapted to new arithmetic simprocs; | changeset | files |
| Fri, 05 May 2000 22:29:02 +0200 | wenzelm | added scan_to_id (used to be in Pure/section_utils.ML); | changeset | files |
| Fri, 05 May 2000 22:25:17 +0200 | wenzelm | removed Pure/section_utils.ML; | changeset | files |
| Fri, 05 May 2000 22:24:47 +0200 | wenzelm | improved syntax of method options (no_asm) etc; | changeset | files |
| Fri, 05 May 2000 22:24:03 +0200 | wenzelm | removed index2; | changeset | files |
| Fri, 05 May 2000 22:23:27 +0200 | wenzelm | updated; | changeset | files |
| Fri, 05 May 2000 22:18:40 +0200 | wenzelm | GPLed; | changeset | files |
| Fri, 05 May 2000 22:09:41 +0200 | wenzelm | GPLed; | changeset | files |
| Fri, 05 May 2000 22:02:46 +0200 | wenzelm | GPLed; | changeset | files |
| Fri, 05 May 2000 22:00:17 +0200 | wenzelm | GPLed; | changeset | files |
| Fri, 05 May 2000 21:59:28 +0200 | wenzelm | GPLed; | changeset | files |
| 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 |
| Sat, 08 Apr 2000 19:38:19 +0200 | wenzelm | fixed comment; | changeset | files |
| Fri, 07 Apr 2000 17:36:56 +0200 | wenzelm | added 'ML_command'; | changeset | files |
| Fri, 07 Apr 2000 17:36:25 +0200 | wenzelm | apply etc.: comments; | changeset | files |
| Thu, 06 Apr 2000 19:11:30 +0200 | wenzelm | tuned \isasymlbrace; | changeset | files |
| Thu, 06 Apr 2000 17:05:38 +0200 | wenzelm | added \isasymlbrace, \isasymrbrace, \isasymtop; | changeset | files |
| Thu, 06 Apr 2000 13:39:49 +0200 | wenzelm | 'welcome' made diagnostic; | changeset | files |
| Wed, 05 Apr 2000 21:08:24 +0200 | wenzelm | added Isar_examples/NestedDatatype.thy; | changeset | files |
| Wed, 05 Apr 2000 21:07:09 +0200 | wenzelm | added NestedDatatype.thy; | changeset | files |
| Wed, 05 Apr 2000 21:06:52 +0200 | wenzelm | added NestedDatatype; | changeset | files |
| Wed, 05 Apr 2000 21:06:37 +0200 | wenzelm | fixed goal selection; | changeset | files |
| Wed, 05 Apr 2000 21:06:06 +0200 | wenzelm | Isar: simplified (more robust) goal selection of proof methods; | changeset | files |
| Wed, 05 Apr 2000 21:05:20 +0200 | wenzelm | induct/case_tac emulation: optional rule; | changeset | files |
| Wed, 05 Apr 2000 21:02:31 +0200 | wenzelm | HEADGOAL; | changeset | files |
| Wed, 05 Apr 2000 21:02:19 +0200 | wenzelm | tuned comment; | changeset | files |
| Wed, 05 Apr 2000 21:01:59 +0200 | wenzelm | removed "as" keyword; | changeset | files |
| Wed, 05 Apr 2000 21:01:33 +0200 | wenzelm | suppress warning; | changeset | files |
| Tue, 04 Apr 2000 22:16:11 +0200 | wenzelm | print_simpset / print_claset command; | changeset | files |
| Tue, 04 Apr 2000 18:08:08 +0200 | wenzelm | case_tac / induct_tac: optional rule; | changeset | files |
| Tue, 04 Apr 2000 12:32:02 +0200 | wenzelm | case_tac, induct_tac; | changeset | files |
| Tue, 04 Apr 2000 12:31:48 +0200 | wenzelm | 'let': replaced 'as' by 'and'; | changeset | files |
| Mon, 03 Apr 2000 21:05:07 +0200 | wenzelm | tuned recover; | changeset | files |
| Mon, 03 Apr 2000 14:02:40 +0200 | wenzelm | isapar, isamarkuptext, isamarkuptxt turned into environments; | changeset | files |
| Mon, 03 Apr 2000 14:00:39 +0200 | wenzelm | markup_env_command 'text' / 'txt'; | changeset | files |
| Mon, 03 Apr 2000 14:00:16 +0200 | wenzelm | support markup environments; | changeset | files |
| Sat, 01 Apr 2000 20:26:20 +0200 | wenzelm | tuned presentation; | changeset | files |
| Sat, 01 Apr 2000 20:22:46 +0200 | wenzelm | proper naming of fib equations; | changeset | files |
| Sat, 01 Apr 2000 20:21:39 +0200 | wenzelm | recdef: admit names/atts; | changeset | files |
| Sat, 01 Apr 2000 20:18:52 +0200 | wenzelm | isatool document: tuned -c option; | changeset | files |
| Sat, 01 Apr 2000 20:17:51 +0200 | wenzelm | recdef: admit name and atts; | changeset | files |
| Sat, 01 Apr 2000 20:16:56 +0200 | wenzelm | tuned -c option; | changeset | files |
| Sat, 01 Apr 2000 20:15:55 +0200 | wenzelm | recover: observe stopper; | changeset | files |
| Sat, 01 Apr 2000 20:13:33 +0200 | wenzelm | presentation ignore stuff: swallow newline; | changeset | files |
| Sat, 01 Apr 2000 20:12:52 +0200 | wenzelm | added is_newline; | changeset | files |
| Sat, 01 Apr 2000 20:12:15 +0200 | wenzelm | 'cd': diag; | changeset | files |
| Sat, 01 Apr 2000 20:11:50 +0200 | wenzelm | more robust handling of explicit rules; | changeset | files |
| Sat, 01 Apr 2000 20:10:57 +0200 | wenzelm | tuned mixfix syntax; | changeset | files |
| Sat, 01 Apr 2000 20:09:52 +0200 | wenzelm | added ProofGeneral.undo; | changeset | files |
| Sat, 01 Apr 2000 20:09:20 +0200 | wenzelm | isatool document: check output file (workaround PolyML problem with RC); | changeset | files |
| Fri, 31 Mar 2000 22:39:39 +0200 | wenzelm | use cong_add_global att; | changeset | files |
| Fri, 31 Mar 2000 22:39:06 +0200 | wenzelm | added cong atts; | changeset | files |
| Fri, 31 Mar 2000 22:22:23 +0200 | wenzelm | added cong atts; | changeset | files |
| Fri, 31 Mar 2000 22:01:01 +0200 | wenzelm | made SML/XL happy; | changeset | files |
| Fri, 31 Mar 2000 22:00:36 +0200 | wenzelm | change_global/local_css move to Provers/clasimp.ML; | changeset | files |
| Fri, 31 Mar 2000 21:59:37 +0200 | wenzelm | setup cong_attrib_setup; | changeset | files |
| Fri, 31 Mar 2000 21:58:34 +0200 | wenzelm | added change_global/local_css; | changeset | files |
| Fri, 31 Mar 2000 21:57:14 +0200 | wenzelm | added 'cong' att; | changeset | files |
| Fri, 31 Mar 2000 21:56:23 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 31 Mar 2000 21:56:13 +0200 | wenzelm | params: preserve case names; | changeset | files |
| Fri, 31 Mar 2000 21:55:51 +0200 | wenzelm | fixed indexing of elim rules; | changeset | files |
| Fri, 31 Mar 2000 21:55:27 +0200 | wenzelm | use Attrib.add_del_args; | changeset | files |
| Fri, 31 Mar 2000 21:54:50 +0200 | wenzelm | added add_del_args; | changeset | files |
| Fri, 31 Mar 2000 18:10:21 +0200 | wenzelm | fixed goal syntax; | changeset | files |
| Fri, 31 Mar 2000 10:23:15 +0200 | nipkow | comments modified | changeset | files |
| Fri, 31 Mar 2000 10:17:32 +0200 | kleing | tuned | changeset | files |
| Fri, 31 Mar 2000 10:15:33 +0200 | kleing | included new stanford mirror, mirror links now point to source directly | changeset | files |
| Fri, 31 Mar 2000 10:08:26 +0200 | nipkow | updated recdef | changeset | files |
| Thu, 30 Mar 2000 21:26:10 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 30 Mar 2000 20:06:27 +0200 | nipkow | recdef | changeset | files |
| Thu, 30 Mar 2000 19:47:17 +0200 | nipkow | If all termination conditions are proved automatically, | changeset | files |
| Thu, 30 Mar 2000 19:45:51 +0200 | nipkow | recdef.rules -> recdef.simps | changeset | files |
| Thu, 30 Mar 2000 19:45:18 +0200 | nipkow | mod in recdef allows to access the correct simpset via simpset(). | changeset | files |
| Thu, 30 Mar 2000 19:44:11 +0200 | nipkow | the simplification rules returned from TFL are now paired with the row they | changeset | files |
| Thu, 30 Mar 2000 15:13:59 +0200 | wenzelm | * Isar/Pure: local results and corresponding term bindings are now | changeset | files |
| Thu, 30 Mar 2000 15:13:02 +0200 | wenzelm | support Hindley-Milner polymorphisms in results and bindings; | changeset | files |
| Thu, 30 Mar 2000 15:12:20 +0200 | wenzelm | added 'moreover' and 'ultimately'; | changeset | files |
| Thu, 30 Mar 2000 15:11:48 +0200 | wenzelm | added \MOREOVER, \ULTIMATELY; | changeset | files |
| Thu, 30 Mar 2000 14:28:54 +0200 | wenzelm | support Hindley-Milner polymorphisms in binds and facts; | changeset | files |
| Thu, 30 Mar 2000 14:28:10 +0200 | wenzelm | support Hindley-Milner polymorphisms in binds and facts; | changeset | files |
| Thu, 30 Mar 2000 14:25:35 +0200 | wenzelm | let_bind(_i): polymorphic version; | changeset | files |
| Thu, 30 Mar 2000 14:24:46 +0200 | wenzelm | ProofContext.find_free; | changeset | files |
| Thu, 30 Mar 2000 14:22:15 +0200 | wenzelm | 'tactic': refer to PureIsar structure; | changeset | files |
| Thu, 30 Mar 2000 14:21:28 +0200 | wenzelm | ?this: support params; | changeset | files |
| Thu, 30 Mar 2000 14:20:42 +0200 | wenzelm | support polymorphic Vars; | changeset | files |
| Thu, 30 Mar 2000 14:20:13 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 30 Mar 2000 14:20:01 +0200 | wenzelm | foldl_term_types: depend on term as well; | changeset | files |
| Thu, 30 Mar 2000 14:19:33 +0200 | wenzelm | read_def_cterms: use Sign.read_def_terms; | changeset | files |
| Thu, 30 Mar 2000 14:19:13 +0200 | wenzelm | read_def_terms (no certify yet); | changeset | files |
| Thu, 30 Mar 2000 14:18:40 +0200 | wenzelm | export update_multi; | changeset | files |
| Thu, 30 Mar 2000 14:15:41 +0200 | wenzelm | added tvars_intr_list; | changeset | files |
| Wed, 29 Mar 2000 15:09:51 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 29 Mar 2000 14:23:27 +0200 | nipkow | *** empty log message *** | changeset | files |
| Tue, 28 Mar 2000 17:33:44 +0200 | nipkow | mods because of weak_case_cong -> removed Action.ML twice | changeset | files |
| Tue, 28 Mar 2000 17:32:24 +0200 | nipkow | added weak_case_cong feature | changeset | files |
| Tue, 28 Mar 2000 17:31:36 +0200 | nipkow | mods because of weak_case_cong | changeset | files |
| Tue, 28 Mar 2000 12:28:24 +0200 | wenzelm | fixed railqtoken; | changeset | files |
| Tue, 28 Mar 2000 11:50:23 +0200 | wenzelm | -I option; | changeset | files |
| Mon, 27 Mar 2000 21:41:19 +0200 | wenzelm | renamed 'hoare_vcg' to 'hoare'; | changeset | files |
| Mon, 27 Mar 2000 21:13:23 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 27 Mar 2000 21:13:06 +0200 | wenzelm | fixed dddot_tr; | changeset | files |
| Mon, 27 Mar 2000 18:10:11 +0200 | wenzelm | rail token vs. terminal; | changeset | files |
| Mon, 27 Mar 2000 18:09:49 +0200 | wenzelm | fixed term syntax; | changeset | files |
| Mon, 27 Mar 2000 18:09:24 +0200 | wenzelm | tail token vs. terminal; | changeset | files |
| Mon, 27 Mar 2000 18:08:57 +0200 | wenzelm | fixed \rail@tokenfont (ever used?); | changeset | files |
| Mon, 27 Mar 2000 17:04:03 +0200 | paulson | added an order-sorted version of quickSort | changeset | files |
| Mon, 27 Mar 2000 16:25:53 +0200 | paulson | simplified constant "colored" | changeset | files |
| Sun, 26 Mar 2000 22:31:11 +0200 | wenzelm | added 'ultimately'; | changeset | files |
| Sun, 26 Mar 2000 22:29:33 +0200 | wenzelm | added WhileRule'; | changeset | files |
| Sun, 26 Mar 2000 20:38:23 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Sun, 26 Mar 2000 20:17:52 +0200 | wenzelm | tuned presentation; | changeset | files |
| Sun, 26 Mar 2000 20:16:34 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 26 Mar 2000 20:13:53 +0200 | wenzelm | ignore_stuff; | changeset | files |
| Sun, 26 Mar 2000 20:12:28 +0200 | wenzelm | tuned output; | changeset | files |
| Sun, 26 Mar 2000 20:11:12 +0200 | wenzelm | !!!! = cut "Corrupted outer syntax in presentation"; | changeset | files |
| Sun, 26 Mar 2000 20:10:31 +0200 | wenzelm | added is_begin/end_ignore; | changeset | files |
| Sun, 26 Mar 2000 20:08:03 +0200 | wenzelm | tuned targets; | changeset | files |
| Sat, 25 Mar 2000 18:01:27 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 25 Mar 2000 17:59:52 +0100 | wenzelm | improved (anti)quote_tr('); | changeset | files |
| Sat, 25 Mar 2000 13:00:44 +0100 | wenzelm | addsimprocs [record_simproc]; | changeset | files |
| Sat, 25 Mar 2000 12:59:31 +0100 | wenzelm | tuned antiquote_tr'; | changeset | files |
| Sat, 25 Mar 2000 12:52:06 +0100 | wenzelm | export updateN; | changeset | files |
| Fri, 24 Mar 2000 21:15:56 +0100 | wenzelm | use abstract syntax; | changeset | files |
| Fri, 24 Mar 2000 21:09:34 +0100 | wenzelm | plain ASCII; | changeset | files |
| Fri, 24 Mar 2000 20:59:15 +0100 | wenzelm | arith method: HEADGOAL; | changeset | files |
| Fri, 24 Mar 2000 17:29:51 +0100 | wenzelm | HOL/ex/Multiquote; | changeset | files |
| Fri, 24 Mar 2000 17:28:03 +0100 | wenzelm | added HOL/ex/Multiquote.thy; | changeset | files |
| Fri, 24 Mar 2000 14:40:51 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 24 Mar 2000 13:48:31 +0100 | wenzelm | usedir -D: update styles as well; | changeset | files |
| Fri, 24 Mar 2000 13:48:01 +0100 | wenzelm | usedir -D: update styles; | changeset | files |
| Fri, 24 Mar 2000 13:47:36 +0100 | wenzelm | improved dump of styles; | changeset | files |
| Fri, 24 Mar 2000 11:52:19 +0100 | wenzelm | -o sty; | changeset | files |
| Fri, 24 Mar 2000 08:56:48 +0100 | nipkow | comments | changeset | files |
| Thu, 23 Mar 2000 21:37:13 +0100 | wenzelm | added 'moreover' command; | changeset | files |
| Thu, 23 Mar 2000 21:36:43 +0100 | wenzelm | tuned output; | changeset | files |
| Thu, 23 Mar 2000 11:28:10 +0100 | wenzelm | tuned spacing; | changeset | files |
| Thu, 23 Mar 2000 11:27:52 +0100 | wenzelm | ex/Antiquote.thy made new-style theory; | changeset | files |
| Thu, 23 Mar 2000 10:23:54 +0100 | paulson | now exclusively uses rtac/dtac/etac rather than the long forms | changeset | files |
| Thu, 23 Mar 2000 10:22:08 +0100 | paulson | restored the MESON examples file HOL/ex/mesontest2.ML | changeset | files |
| Wed, 22 Mar 2000 13:23:57 +0100 | paulson | made a proof more robust (did not like Suc_less_eq) | changeset | files |
| Wed, 22 Mar 2000 13:22:39 +0100 | paulson | Suc_less_eq now with AddIffs. How could this have been overlooked? | changeset | files |
| Wed, 22 Mar 2000 13:22:11 +0100 | paulson | combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the | changeset | files |
| Wed, 22 Mar 2000 13:01:57 +0100 | paulson | made more robust | changeset | files |
| Wed, 22 Mar 2000 13:01:18 +0100 | paulson | tidied using new "inst" rule | changeset | files |
| Wed, 22 Mar 2000 12:45:41 +0100 | paulson | tidied using new "inst" rule | changeset | files |
| Wed, 22 Mar 2000 12:33:34 +0100 | paulson | new meta-rule "inst", a shorthand for read_instantiate_sg | changeset | files |
| Tue, 21 Mar 2000 17:43:54 +0100 | wenzelm | goal_spec: [!]; | changeset | files |
| Tue, 21 Mar 2000 17:32:44 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 21 Mar 2000 17:32:43 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 21 Mar 2000 15:32:08 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 21 Mar 2000 15:26:21 +0100 | wenzelm | tuned comment; | changeset | files |
| Tue, 21 Mar 2000 15:23:33 +0100 | wenzelm | help message; | changeset | files |
| Tue, 21 Mar 2000 00:18:54 +0100 | wenzelm | handle general case: params and hyps of thesis; | changeset | files |
| Tue, 21 Mar 2000 00:17:56 +0100 | wenzelm | soft_asm_tac: hack to norm goal; | changeset | files |
| Mon, 20 Mar 2000 18:49:14 +0100 | wenzelm | proof methods: 'case_tac' / 'induct_tac'; | changeset | files |
| Mon, 20 Mar 2000 18:48:43 +0100 | wenzelm | tuned degenerate cases / induct; | changeset | files |
| Mon, 20 Mar 2000 18:48:12 +0100 | wenzelm | added prove_goalw_cterm; | changeset | files |
| Mon, 20 Mar 2000 18:47:47 +0100 | wenzelm | quick_and_dirty moved to Isar/skip_proof.ML; | changeset | files |
| Mon, 20 Mar 2000 18:47:27 +0100 | wenzelm | use Args.goal_spec; | changeset | files |
| Mon, 20 Mar 2000 18:47:07 +0100 | wenzelm | goal_spec; | changeset | files |
| Mon, 20 Mar 2000 18:46:53 +0100 | wenzelm | ALLGOALS_RANGE superceded by Seq.INTERVAL; | changeset | files |
| Mon, 20 Mar 2000 18:45:28 +0100 | wenzelm | improved support for emulating tactic scripts; | changeset | files |
| Mon, 20 Mar 2000 18:43:37 +0100 | wenzelm | res_inst_tac etc.; | changeset | files |
| Mon, 20 Mar 2000 18:43:20 +0100 | wenzelm | goalspec; | changeset | files |
| Mon, 20 Mar 2000 18:43:05 +0100 | wenzelm | case_tac, induct_tac; | changeset | files |
| Mon, 20 Mar 2000 18:42:50 +0100 | wenzelm | tactic emulation; | changeset | files |
| Mon, 20 Mar 2000 18:25:35 +0100 | paulson | tidied | changeset | files |
| Mon, 20 Mar 2000 18:24:11 +0100 | paulson | the perm_rules variable is no longer needed | changeset | files |
| Mon, 20 Mar 2000 12:54:31 +0100 | paulson | tidied | changeset | files |
| Mon, 20 Mar 2000 11:15:28 +0100 | paulson | replaced best_tac by force_tac, allowing some arithmetic reasoning | changeset | files |
| Mon, 20 Mar 2000 10:32:02 +0100 | paulson | renamed a variable to avoid possible free/bound confusion | changeset | files |
| Mon, 20 Mar 2000 10:26:34 +0100 | paulson | a possibly (?) more perspicous simprule in the "simpset" part | changeset | files |
| Mon, 20 Mar 2000 10:24:07 +0100 | paulson | now based on "Main", as it should be | changeset | files |
| Mon, 20 Mar 2000 10:23:24 +0100 | paulson | deleted unnecessary "simpset" part from recdef | changeset | files |
| Sat, 18 Mar 2000 19:20:10 +0100 | wenzelm | 'oops' made proper; | changeset | files |
| Sat, 18 Mar 2000 19:19:53 +0100 | wenzelm | intro_classes_tac: REPEAT_ALL_NEW; | changeset | files |
| Sat, 18 Mar 2000 19:18:48 +0100 | wenzelm | tuned comments; | changeset | files |
| Sat, 18 Mar 2000 19:16:56 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 18 Mar 2000 19:11:34 +0100 | wenzelm | obtain; | changeset | files |
| Sat, 18 Mar 2000 19:10:02 +0100 | wenzelm | simplified setup; | changeset | files |
| Sat, 18 Mar 2000 19:07:47 +0100 | wenzelm | pure methods / atts moved here; | changeset | files |
| Sat, 18 Mar 2000 19:04:32 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 18 Mar 2000 19:03:57 +0100 | wenzelm | obtain; | changeset | files |
| Fri, 17 Mar 2000 22:53:19 +0100 | wenzelm | parskip 0pt; | changeset | files |
| Fri, 17 Mar 2000 22:52:29 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 17 Mar 2000 22:52:14 +0100 | wenzelm | fixed theory, context typing; | changeset | files |
| Fri, 17 Mar 2000 22:51:24 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 17 Mar 2000 22:51:05 +0100 | wenzelm | simplified Proof General setup; | changeset | files |
| Fri, 17 Mar 2000 22:50:41 +0100 | wenzelm | untag: only name arg; | changeset | files |
| Fri, 17 Mar 2000 22:50:04 +0100 | wenzelm | arith: "!" arg; | changeset | files |
| Fri, 17 Mar 2000 22:49:44 +0100 | wenzelm | x-symbol; | changeset | files |
| Fri, 17 Mar 2000 22:49:13 +0100 | wenzelm | fixed \OBTAIN; | changeset | files |
| Fri, 17 Mar 2000 17:12:07 +0100 | wenzelm | fixed dep; | changeset | files |
| Fri, 17 Mar 2000 17:11:59 +0100 | wenzelm | arith method: bang arg; | changeset | files |
| Fri, 17 Mar 2000 17:10:37 +0100 | wenzelm | \isamarkupheader: \section; | changeset | files |
| Fri, 17 Mar 2000 16:31:06 +0100 | wenzelm | generic "kill" command; | changeset | files |
| Fri, 17 Mar 2000 16:30:45 +0100 | wenzelm | old_symbol_source: include header; | changeset | files |
| Fri, 17 Mar 2000 16:30:03 +0100 | wenzelm | kill: include kill_proof; | changeset | files |
| Fri, 17 Mar 2000 16:29:35 +0100 | wenzelm | fixed untag; | changeset | files |
| Fri, 17 Mar 2000 16:28:59 +0100 | wenzelm | untag: remove all tags of given name; | changeset | files |
| Fri, 17 Mar 2000 16:27:28 +0100 | wenzelm | no begin_goal marker (interferes with "latex" etc. output; useless anyway?) | changeset | files |
| Fri, 17 Mar 2000 16:26:43 +0100 | wenzelm | next_block: allow in non-goal blocks as well (experimental); | changeset | files |
| Fri, 17 Mar 2000 15:51:13 +0100 | paulson | re-ordered the theorems | changeset | files |
| Fri, 17 Mar 2000 15:49:50 +0100 | paulson | better error messages, especially for multiple types | changeset | files |
| Thu, 16 Mar 2000 00:36:22 +0100 | wenzelm | Splitter support; | changeset | files |
| Thu, 16 Mar 2000 00:35:27 +0100 | wenzelm | added HOL/PreLIst.thy; | changeset | files |
| Thu, 16 Mar 2000 00:33:46 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 16 Mar 2000 00:32:55 +0100 | wenzelm | do not change parindent/parskip; | changeset | files |
| Thu, 16 Mar 2000 00:31:58 +0100 | wenzelm | Isar: splitter support; improved diagnostics; | changeset | files |
| Thu, 16 Mar 2000 00:29:03 +0100 | wenzelm | Splitter support; | changeset | files |
| Thu, 16 Mar 2000 00:28:35 +0100 | wenzelm | moved "cases" to generic.tex; | changeset | files |
| Thu, 16 Mar 2000 00:27:02 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 16 Mar 2000 00:26:44 +0100 | wenzelm | Named local contexts (cases); | changeset | files |
| Wed, 15 Mar 2000 23:41:42 +0100 | berghofe | Added setup for primrec theory data. | changeset | files |
| Wed, 15 Mar 2000 23:40:59 +0100 | berghofe | get_recdef now returns None instead of raising ERROR. | changeset | files |
| Wed, 15 Mar 2000 23:39:45 +0100 | berghofe | Added new theory data slot for primrec equations. | changeset | files |
| Wed, 15 Mar 2000 23:38:52 +0100 | berghofe | Now returns theorems with correct names in derivations. | changeset | files |
| Wed, 15 Mar 2000 23:38:19 +0100 | berghofe | Eliminated store_clasimp. | changeset | files |
| Wed, 15 Mar 2000 23:36:46 +0100 | berghofe | - Fixed bug in prove_casedist_thms (proof failed because of | changeset | files |
| Wed, 15 Mar 2000 18:52:07 +0100 | wenzelm | made SML/XL happy; | changeset | files |
| Wed, 15 Mar 2000 18:50:48 +0100 | wenzelm | ## -D document; | changeset | files |
| Wed, 15 Mar 2000 18:50:14 +0100 | wenzelm | renamed isabelle env; | changeset | files |
| Wed, 15 Mar 2000 18:47:28 +0100 | wenzelm | splitter setup; | changeset | files |
| Wed, 15 Mar 2000 18:42:54 +0100 | wenzelm | clasimp: include Splitter; | changeset | files |
| Wed, 15 Mar 2000 18:42:13 +0100 | wenzelm | splitter setup; | changeset | files |
| Wed, 15 Mar 2000 18:41:00 +0100 | wenzelm | tuned comments; | changeset | files |
| Wed, 15 Mar 2000 18:40:03 +0100 | wenzelm | include Splitter.split_modifiers; | changeset | files |
| Wed, 15 Mar 2000 18:38:52 +0100 | wenzelm | added attributes, method modifiers, theory setup; | changeset | files |
| Wed, 15 Mar 2000 18:36:53 +0100 | wenzelm | export change_global_ss, change_local_ss; | changeset | files |
| Wed, 15 Mar 2000 18:33:41 +0100 | wenzelm | removed export_chain; | changeset | files |
| Wed, 15 Mar 2000 18:32:41 +0100 | wenzelm | eliminated toplevel stack; | changeset | files |
| Wed, 15 Mar 2000 18:30:45 +0100 | wenzelm | 'pr': modes, optional limit; | changeset | files |
| Wed, 15 Mar 2000 18:29:32 +0100 | wenzelm | pr: modes, optional limit; | changeset | files |
| Wed, 15 Mar 2000 18:26:53 +0100 | wenzelm | pretty chunks; | changeset | files |
| Wed, 15 Mar 2000 18:25:42 +0100 | wenzelm | tuned comment; | changeset | files |
| Wed, 15 Mar 2000 18:24:27 +0100 | wenzelm | tuned comments; | changeset | files |
| Wed, 15 Mar 2000 18:22:39 +0100 | wenzelm | added pretty_goals(_marker); | changeset | files |
| Wed, 15 Mar 2000 18:20:52 +0100 | wenzelm | removed Pretty.spc; | changeset | files |
| Wed, 15 Mar 2000 18:19:06 +0100 | wenzelm | use Pretty.str / Pretty.raw_str; | changeset | files |
| Wed, 15 Mar 2000 18:18:12 +0100 | wenzelm | removed lst, strlen, strlen_real, spc, sym; | changeset | files |
| Wed, 15 Mar 2000 12:05:03 +0100 | kleing | made links to homepages absolute, avoids trouble with relative links on the | changeset | files |
| Tue, 14 Mar 2000 22:58:59 +0100 | wenzelm | 'undo' prints state (again); | changeset | files |
| Tue, 14 Mar 2000 22:58:20 +0100 | wenzelm | pr, disable_pr, enable_pr; | changeset | files |
| Tue, 14 Mar 2000 22:57:54 +0100 | wenzelm | silence undo command; | changeset | files |
| Tue, 14 Mar 2000 11:33:30 +0100 | wenzelm | tuned comments; | changeset | files |
| Tue, 14 Mar 2000 11:33:14 +0100 | wenzelm | invoke_case: include attributes; | changeset | files |
| Tue, 14 Mar 2000 11:32:38 +0100 | wenzelm | 'cases' and 'induct' methods; | changeset | files |
| Tue, 14 Mar 2000 11:31:45 +0100 | wenzelm | tuned 'case'; | changeset | files |
| Tue, 14 Mar 2000 11:31:04 +0100 | wenzelm | added 'case' command; | changeset | files |
| Tue, 14 Mar 2000 11:27:38 +0100 | wenzelm | added \NEXT; | changeset | files |
| Mon, 13 Mar 2000 23:01:09 +0100 | wenzelm | proper symbol_output for "xsymbols" mode; | changeset | files |
| Mon, 13 Mar 2000 16:24:52 +0100 | wenzelm | replaced exhaust_tac by case_tac; | changeset | files |
| Mon, 13 Mar 2000 16:24:23 +0100 | wenzelm | renamed cases_tac to case_tac; | changeset | files |
| Mon, 13 Mar 2000 16:23:34 +0100 | wenzelm | case_tac now subsumes both boolean and datatype cases; | changeset | files |
| Mon, 13 Mar 2000 15:42:19 +0100 | wenzelm | use cases; | changeset | files |
| Mon, 13 Mar 2000 13:34:09 +0100 | wenzelm | * HOL: exhaust_tac on datatypes superceded by new case_tac; | changeset | files |
| Mon, 13 Mar 2000 13:30:49 +0100 | wenzelm | renamed cases_tac to case_tac; | changeset | files |
| Mon, 13 Mar 2000 13:28:31 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:27:44 +0100 | wenzelm | removed cases_of; | changeset | files |
| Mon, 13 Mar 2000 13:24:12 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:22:31 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:21:39 +0100 | wenzelm | use HOLogic.Not; | changeset | files |
| Mon, 13 Mar 2000 13:20:51 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:20:13 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:19:14 +0100 | wenzelm | export vars_of; | changeset | files |
| Mon, 13 Mar 2000 13:18:59 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:17:52 +0100 | wenzelm | added Not; | changeset | files |
| Mon, 13 Mar 2000 13:16:57 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 13:16:43 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 13 Mar 2000 13:16:26 +0100 | wenzelm | cases: preserve order; | changeset | files |
| Mon, 13 Mar 2000 13:13:46 +0100 | nipkow | *** empty log message *** | changeset | files |