| 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 |
| Mon, 13 Mar 2000 13:11:16 +0100 | nipkow | exhaust -> cases | changeset | files |
| Mon, 13 Mar 2000 12:51:10 +0100 | nipkow | exhaust_tac -> cases_tac | changeset | files |
| Mon, 13 Mar 2000 12:42:41 +0100 | paulson | renamed "f" to "le" and "mset" to "multiset" | changeset | files |
| Mon, 13 Mar 2000 12:42:05 +0100 | paulson | fixed the goal statement of sorted_qsort | changeset | files |
| Mon, 13 Mar 2000 12:25:52 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | changeset | files |
| Mon, 13 Mar 2000 12:25:16 +0100 | wenzelm | add_thms, add_axioms, add_defs: return theorems as well; | changeset | files |
| Mon, 13 Mar 2000 12:23:44 +0100 | wenzelm | added |>> and |>>>; | changeset | files |
| Mon, 13 Mar 2000 09:08:27 +0100 | nipkow | exhaust->cases | changeset | files |
| Fri, 10 Mar 2000 23:04:07 +0100 | berghofe | Type.typ_match now uses Vartab instead of association lists. | changeset | files |
| Fri, 10 Mar 2000 17:53:16 +0100 | paulson | tidied | changeset | files |
| Fri, 10 Mar 2000 17:52:48 +0100 | paulson | now uses recdef instead of "rules" | changeset | files |
| Fri, 10 Mar 2000 17:51:59 +0100 | paulson | tidied, and new thm perm_append2_eq | changeset | files |
| Fri, 10 Mar 2000 17:14:56 +0100 | nipkow | cases_tac | changeset | files |
| Fri, 10 Mar 2000 15:03:05 +0100 | berghofe | Type.typ_match now uses Vartab instead of association lists. | changeset | files |
| Fri, 10 Mar 2000 15:02:04 +0100 | berghofe | Type.unify now uses Vartab instead of association lists. | changeset | files |
| Fri, 10 Mar 2000 15:00:32 +0100 | berghofe | Added function min_key. | changeset | files |
| Fri, 10 Mar 2000 15:00:01 +0100 | berghofe | Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab. | changeset | files |
| Fri, 10 Mar 2000 14:58:25 +0100 | berghofe | Envir now uses Vartab instead of association lists. | changeset | files |
| Fri, 10 Mar 2000 14:57:06 +0100 | berghofe | Type.unify and Type.typ_match now use Vartab instead of association lists. | changeset | files |
| Fri, 10 Mar 2000 01:16:19 +0100 | wenzelm | add_cases_induct: produce proper case names; | changeset | files |
| Fri, 10 Mar 2000 01:13:37 +0100 | wenzelm | type descr; | changeset | files |
| Thu, 09 Mar 2000 22:58:23 +0100 | wenzelm | check_case: disallow (T)Vars in invoked case; | changeset | files |
| Thu, 09 Mar 2000 22:57:39 +0100 | wenzelm | quote tag arguments; | changeset | files |
| Thu, 09 Mar 2000 22:57:13 +0100 | wenzelm | more robust case names of induct; | changeset | files |
| Thu, 09 Mar 2000 22:56:40 +0100 | wenzelm | cleaned comment; | changeset | files |
| Thu, 09 Mar 2000 18:27:18 +0100 | paulson | nicely tarted up Mutil | changeset | files |
| Thu, 09 Mar 2000 17:27:54 +0100 | wenzelm | renamed to rsync-isabelle; | changeset | files |
| Thu, 09 Mar 2000 17:25:28 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 09 Mar 2000 17:19:49 +0100 | kleing | made rsync "official" | changeset | files |
| Thu, 09 Mar 2000 16:14:37 +0100 | paulson | mod_less, div_less are now default simprules | changeset | files |
| Thu, 09 Mar 2000 16:09:56 +0100 | kleing | moved more lemmas to Convert (transitivity etc) | changeset | files |
| Thu, 09 Mar 2000 16:07:38 +0100 | paulson | mod_less, div_less are now default simprules | changeset | files |
| Thu, 09 Mar 2000 16:07:01 +0100 | paulson | Factorization | changeset | files |
| Thu, 09 Mar 2000 14:19:15 +0100 | kleing | rsync goes "official" (started at boot time) | changeset | files |
| Thu, 09 Mar 2000 13:56:54 +0100 | kleing | tuned for completeness of LBV | changeset | files |
| Thu, 09 Mar 2000 13:55:39 +0100 | kleing | some more small lemmas | changeset | files |
| Thu, 09 Mar 2000 13:54:03 +0100 | kleing | completeness of the lightweight bytecode verifier | changeset | files |
| Thu, 09 Mar 2000 13:51:53 +0100 | kleing | added NT case for method invocation | changeset | files |
| Thu, 09 Mar 2000 13:50:58 +0100 | kleing | minor adjustments in branch and method invocation for completeness of LBV | changeset | files |
| Thu, 09 Mar 2000 10:35:07 +0100 | paulson | updated discussion of compilers | changeset | files |
| Wed, 08 Mar 2000 23:49:30 +0100 | wenzelm | add_cases: omit unnamed; | changeset | files |
| Wed, 08 Mar 2000 23:48:34 +0100 | wenzelm | invoke_case: name assumption; | changeset | files |
| Wed, 08 Mar 2000 23:47:44 +0100 | wenzelm | fixed section syntax; | changeset | files |
| Wed, 08 Mar 2000 23:46:59 +0100 | wenzelm | sect: exlude ":" from parser; | changeset | files |
| Wed, 08 Mar 2000 23:45:37 +0100 | wenzelm | removed tune_names; | changeset | files |
| Wed, 08 Mar 2000 23:43:11 +0100 | wenzelm | tuned ML types; | changeset | files |
| Wed, 08 Mar 2000 23:40:48 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 08 Mar 2000 23:37:25 +0100 | wenzelm | added \CASE, \OBTAIN, \SORRY, \OOPS; | changeset | files |
| Wed, 08 Mar 2000 18:08:08 +0100 | wenzelm | added dest_global/local_rules; | changeset | files |
| Wed, 08 Mar 2000 18:06:12 +0100 | wenzelm | mk_elims, add_cases_induct: name rule cases; | changeset | files |
| Wed, 08 Mar 2000 18:02:36 +0100 | wenzelm | generalized FINDGOAL, HEADGOAL; | changeset | files |
| Wed, 08 Mar 2000 18:00:01 +0100 | wenzelm | handling of local contexts: print_cases, get_case, add_cases; | changeset | files |
| Wed, 08 Mar 2000 17:58:37 +0100 | wenzelm | added METHOD_CASES, resolveq_cases_tac; | changeset | files |
| Wed, 08 Mar 2000 17:56:43 +0100 | wenzelm | added invoke_case; | changeset | files |
| Wed, 08 Mar 2000 17:55:17 +0100 | wenzelm | added 'case' command; | changeset | files |
| Wed, 08 Mar 2000 17:54:25 +0100 | wenzelm | added print_cases; | changeset | files |
| Wed, 08 Mar 2000 17:52:38 +0100 | wenzelm | added 'case_names' and 'params'; | changeset | files |
| Wed, 08 Mar 2000 17:51:29 +0100 | wenzelm | added rule_cases.ML; | changeset | files |
| Wed, 08 Mar 2000 17:50:28 +0100 | wenzelm | export ALLGOALS_RANGE; | changeset | files |
| Wed, 08 Mar 2000 17:49:28 +0100 | wenzelm | added (un)tag_rule; | changeset | files |
| Wed, 08 Mar 2000 17:48:31 +0100 | wenzelm | added Isar/rule_cases.ML; | changeset | files |
| Wed, 08 Mar 2000 17:45:16 +0100 | wenzelm | added isatool mkdir; | changeset | files |
| Wed, 08 Mar 2000 17:44:53 +0100 | wenzelm | isabelle -c: tell ML system to compress output image; | changeset | files |
| Wed, 08 Mar 2000 17:41:40 +0100 | wenzelm | pass -c option; | changeset | files |
| Wed, 08 Mar 2000 17:40:24 +0100 | wenzelm | observe COMPRESS option; | changeset | files |
| Wed, 08 Mar 2000 17:39:08 +0100 | wenzelm | option -c: tell ML system to compress output image; | changeset | files |
| Wed, 08 Mar 2000 17:36:54 +0100 | wenzelm | * isatool mkdir provides easy setup of Isabelle session directories, | changeset | files |
| Wed, 08 Mar 2000 17:35:08 +0100 | wenzelm | tuned error msg: rows counted from 1; | changeset | files |
| Wed, 08 Mar 2000 16:24:46 +0100 | paulson | tidied | changeset | files |
| Wed, 08 Mar 2000 16:17:10 +0100 | paulson | tidied | changeset | files |
| Wed, 08 Mar 2000 16:15:41 +0100 | paulson | function "remove" and new lemmas for Factorization | changeset | files |
| Wed, 08 Mar 2000 16:14:12 +0100 | paulson | new theory ex/Factorization | changeset | files |
| Wed, 08 Mar 2000 16:13:19 +0100 | paulson | new lemmas | changeset | files |
| Mon, 06 Mar 2000 21:10:27 +0100 | wenzelm | added simple_args; | changeset | files |
| Mon, 06 Mar 2000 21:09:37 +0100 | wenzelm | argument: include verbatim; | changeset | files |
| Mon, 06 Mar 2000 21:08:36 +0100 | wenzelm | moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML; | changeset | files |
| Mon, 06 Mar 2000 21:08:15 +0100 | wenzelm | added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML); | changeset | files |
| Mon, 06 Mar 2000 15:44:51 +0100 | wenzelm | rsyncd setup; | changeset | files |
| Mon, 06 Mar 2000 15:24:07 +0100 | kleing | switched to mirroring with rsync server | changeset | files |
| Mon, 06 Mar 2000 12:04:39 +0100 | wenzelm | new Poly/ML setup made default; | changeset | files |
| Sat, 04 Mar 2000 13:28:21 +0100 | wenzelm | induct: "stripped" option; | changeset | files |
| Sat, 04 Mar 2000 13:25:09 +0100 | wenzelm | require NatDef; | changeset | files |
| Sat, 04 Mar 2000 13:23:07 +0100 | wenzelm | REPEAT_ALL_NEW; | changeset | files |
| Sat, 04 Mar 2000 13:18:43 +0100 | wenzelm | added REPEAT_ALL_NEW; | changeset | files |
| Sat, 04 Mar 2000 12:02:41 +0100 | paulson | tidied | changeset | files |
| Sat, 04 Mar 2000 11:52:42 +0100 | paulson | tidied | changeset | files |
| Sat, 04 Mar 2000 11:42:12 +0100 | paulson | new theories UNITY/Detects, UNITY/Reachability | changeset | files |
| Fri, 03 Mar 2000 21:02:45 +0100 | wenzelm | added con_elim_s(olved_)tac; | changeset | files |
| Fri, 03 Mar 2000 21:01:57 +0100 | wenzelm | mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac; | changeset | files |
| Fri, 03 Mar 2000 21:00:58 +0100 | wenzelm | added multi_resolveq, resolveq_tac; | changeset | files |
| Fri, 03 Mar 2000 18:26:19 +0100 | paulson | Added Tanja's Detects and Reachability theories. Also | changeset | files |
| Fri, 03 Mar 2000 18:22:53 +0100 | paulson | improved reasoning about {} and UNIV | changeset | files |
| Fri, 03 Mar 2000 02:00:43 +0100 | wenzelm | join_rules: compatibility check; | changeset | files |
| Fri, 03 Mar 2000 01:58:57 +0100 | wenzelm | token_trans: symbol length; | changeset | files |
| Thu, 02 Mar 2000 18:18:59 +0100 | wenzelm | join induct rules; | changeset | files |
| Thu, 02 Mar 2000 18:18:31 +0100 | wenzelm | added 'prolog' method; | changeset | files |
| Thu, 02 Mar 2000 18:18:10 +0100 | wenzelm | added freeze_all; | changeset | files |
| Thu, 02 Mar 2000 10:29:29 +0100 | paulson | polished version of the Allocator using Rename | changeset | files |
| Thu, 02 Mar 2000 10:26:22 +0100 | paulson | tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and | changeset | files |
| Wed, 01 Mar 2000 20:49:13 +0100 | wenzelm | project induct rule; | changeset | files |
| Wed, 01 Mar 2000 20:48:57 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 01 Mar 2000 16:40:14 +0100 | wenzelm | test setup; | changeset | files |
| Wed, 01 Mar 2000 16:39:17 +0100 | wenzelm | proper setup; | changeset | files |
| Wed, 01 Mar 2000 16:38:59 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 01 Mar 2000 15:00:21 +0100 | paulson | expandshort | changeset | files |
| Wed, 01 Mar 2000 12:26:28 +0100 | paulson | added a reference | changeset | files |
| Wed, 01 Mar 2000 12:18:40 +0100 | paulson | new theorems from Sidi Ould Ehmety | changeset | files |
| Tue, 29 Feb 2000 23:08:27 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 29 Feb 2000 23:06:20 +0100 | wenzelm | add_cases_induct: project_rules accomodates mutual induction; | changeset | files |
| Tue, 29 Feb 2000 20:51:43 +0100 | wenzelm | tuned msgs; | changeset | files |
| Tue, 29 Feb 2000 10:57:30 +0100 | paulson | even Alloc works again, using "rename" | changeset | files |
| Tue, 29 Feb 2000 10:41:08 +0100 | paulson | replaced UN_constant, INT_constant by unconditional versions that rewrite | changeset | files |
| Mon, 28 Feb 2000 13:39:45 +0100 | wenzelm | add_cases_induct: accomodate no_elim and no_ind flags; | changeset | files |
| Mon, 28 Feb 2000 10:49:42 +0100 | paulson | new mostly working version; Alloc nearly converted to "Rename" | changeset | files |
| Mon, 28 Feb 2000 10:49:08 +0100 | paulson | new thm vimage_Collect_eq | changeset | files |
| Mon, 28 Feb 2000 10:48:39 +0100 | paulson | more bijection theorems | changeset | files |
| Sun, 27 Feb 2000 15:33:35 +0100 | wenzelm | cases/induct attributes; | changeset | files |
| Sun, 27 Feb 2000 15:32:10 +0100 | wenzelm | add_cases_induct: induct_method setup; | changeset | files |
| Sun, 27 Feb 2000 15:31:40 +0100 | wenzelm | HOLogic.dest_conj; | changeset | files |
| Sun, 27 Feb 2000 15:26:47 +0100 | wenzelm | HOLogic.dest_conj; | changeset | files |
| Sun, 27 Feb 2000 15:25:31 +0100 | wenzelm | even better induct setup; | changeset | files |
| Sun, 27 Feb 2000 15:23:28 +0100 | wenzelm | early setup of induct_method; | changeset | files |
| Sun, 27 Feb 2000 15:22:14 +0100 | wenzelm | added dest_conj; | changeset | files |
| Sun, 27 Feb 2000 15:21:13 +0100 | wenzelm | theorems [trans] = rev_mp mp; | changeset | files |
| Sun, 27 Feb 2000 15:15:52 +0100 | wenzelm | use NetRules; | changeset | files |
| Sun, 27 Feb 2000 15:13:44 +0100 | wenzelm | added major_prem_of; | changeset | files |
| Sun, 27 Feb 2000 15:07:53 +0100 | wenzelm | added Isar/net_rules.ML; | changeset | files |
| Thu, 24 Feb 2000 21:33:32 +0100 | wenzelm | simplified induct method; | changeset | files |
| Thu, 24 Feb 2000 16:04:25 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 24 Feb 2000 16:01:34 +0100 | wenzelm | induct method: implicit rule; | changeset | files |
| Thu, 24 Feb 2000 16:00:28 +0100 | wenzelm | rN = "record"; | changeset | files |
| Thu, 24 Feb 2000 16:00:09 +0100 | wenzelm | all_cases / all_inducts; | changeset | files |
| Thu, 24 Feb 2000 15:59:44 +0100 | wenzelm | workaround res_inst_tac/lift_inst_rule bug by explicit type contraint; | changeset | files |
| Thu, 24 Feb 2000 15:58:10 +0100 | wenzelm | capply, cabs: Sign.nodup_vars; | changeset | files |
| Thu, 24 Feb 2000 15:57:36 +0100 | wenzelm | nodup_vars: fixed omission of 2 minor cases; account for Frees as well; | changeset | files |
| Thu, 24 Feb 2000 15:34:49 +0100 | wenzelm | tuned generated TeX code; | changeset | files |
| Thu, 24 Feb 2000 08:56:36 +0100 | nipkow | renamed a lemma | changeset | files |
| Thu, 24 Feb 2000 08:55:37 +0100 | nipkow | Added and renamed a lemma. | changeset | files |
| Wed, 23 Feb 2000 10:45:08 +0100 | paulson | not working yet. partial conversion to use "rename" instead of "extend" | changeset | files |
| Wed, 23 Feb 2000 10:43:02 +0100 | paulson | new theorems inj_iff, surj_iff | changeset | files |
| Wed, 23 Feb 2000 10:41:37 +0100 | paulson | new reference korf85 | changeset | files |
| Tue, 22 Feb 2000 21:53:17 +0100 | wenzelm | * Pure now provides its own version of intro/elim/dest attributes; | changeset | files |
| Tue, 22 Feb 2000 21:51:25 +0100 | wenzelm | tuned syntax wrapper; | changeset | files |
| Tue, 22 Feb 2000 21:50:02 +0100 | wenzelm | tuned "induct" syntax; | changeset | files |
| Tue, 22 Feb 2000 21:49:34 +0100 | wenzelm | "cases" method; | changeset | files |
| Tue, 22 Feb 2000 21:48:50 +0100 | wenzelm | added cases_tac; | changeset | files |
| Tue, 22 Feb 2000 21:48:24 +0100 | wenzelm | induct: tuned syntax; | changeset | files |
| Tue, 22 Feb 2000 21:45:20 +0100 | wenzelm | added cases_of, cases; | changeset | files |
| Tue, 22 Feb 2000 21:39:38 +0100 | wenzelm | removed case_split thm binding; | changeset | files |
| Tue, 22 Feb 2000 21:39:01 +0100 | wenzelm | added boolN; | changeset | files |
| Tue, 22 Feb 2000 20:16:07 +0100 | wenzelm | proper variant names (admit field "r"); | changeset | files |
| Tue, 22 Feb 2000 10:51:13 +0100 | paulson | three easy new examples | changeset | files |
| Mon, 21 Feb 2000 14:10:21 +0100 | wenzelm | tuned footnote; | changeset | files |
| Mon, 21 Feb 2000 14:09:40 +0100 | wenzelm | HOL/record: fixed select-update simplification procedure to handle | changeset | files |
| Mon, 21 Feb 2000 14:09:18 +0100 | wenzelm | var: skolem; | changeset | files |
| Mon, 21 Feb 2000 14:08:15 +0100 | wenzelm | remove *.out; | changeset | files |
| Mon, 21 Feb 2000 13:57:07 +0100 | oheimb | renamed Univalent to univalent | changeset | files |
| Mon, 21 Feb 2000 11:16:19 +0100 | paulson | simplified some proofs | changeset | files |
| Mon, 21 Feb 2000 11:15:43 +0100 | paulson | new examples that cannot be done in LEO | changeset | files |
| Mon, 21 Feb 2000 10:20:38 +0100 | nipkow | A few lemmas and some Adds. | changeset | files |
| Sun, 20 Feb 2000 09:32:06 +0100 | nipkow | Added global let-simplification rule. | changeset | files |
| Sat, 19 Feb 2000 13:47:12 +0100 | nipkow | Commenst. | changeset | files |
| Fri, 18 Feb 2000 20:27:19 +0100 | oheimb | added instance declaration for finite product | changeset | files |
| Fri, 18 Feb 2000 20:25:29 +0100 | oheimb | added split_eta_SetCompr, SetCompr_Sigma_eq | changeset | files |
| Fri, 18 Feb 2000 20:24:56 +0100 | oheimb | added Suc_le_D | changeset | files |
| Fri, 18 Feb 2000 20:24:40 +0100 | oheimb | added domI, domD | changeset | files |
| Fri, 18 Feb 2000 20:24:16 +0100 | oheimb | changed precedence of function update | changeset | files |
| Fri, 18 Feb 2000 18:29:28 +0100 | nipkow | installed lin arith for nat numerals. | changeset | files |
| Fri, 18 Feb 2000 15:37:08 +0100 | paulson | Rename: theory for applying a bijection over states to a UNITY program | changeset | files |
| Fri, 18 Feb 2000 15:35:29 +0100 | paulson | new distributive laws | changeset | files |
| Fri, 18 Feb 2000 15:34:22 +0100 | paulson | expandshort | changeset | files |
| Fri, 18 Feb 2000 15:33:09 +0100 | paulson | many new theorems about inj, surj etc. | changeset | files |
| Fri, 18 Feb 2000 15:28:32 +0100 | paulson | new theorem nat_diff_split' | changeset | files |
| Fri, 18 Feb 2000 15:20:44 +0100 | paulson | New treatment of "guarantees" with polymorphic components and bijections. | changeset | files |
| Wed, 16 Feb 2000 15:04:12 +0100 | wenzelm | Syntax translation functions; | changeset | files |
| Wed, 16 Feb 2000 10:51:23 +0100 | paulson | fixed some overfull lines | changeset | files |
| Wed, 16 Feb 2000 10:50:57 +0100 | paulson | a smaller point size reduces the number of overfull figures | changeset | files |
| Tue, 15 Feb 2000 21:02:55 +0100 | kleing | cosmetics | changeset | files |
| Tue, 15 Feb 2000 19:41:44 +0100 | wenzelm | fixed sel_upd simproc (less efficient, but more complete); | changeset | files |
| Tue, 15 Feb 2000 17:51:11 +0100 | kleing | lightweight bytecode verifier with correctness proof | changeset | files |
| Mon, 14 Feb 2000 20:49:08 +0100 | wenzelm | basic source deps; | changeset | files |
| Mon, 14 Feb 2000 20:43:12 +0100 | wenzelm | easy_setup: fixed mksimps; | changeset | files |
| Mon, 14 Feb 2000 20:42:02 +0100 | wenzelm | proof step: reset goal_facts; | changeset | files |
| Mon, 14 Feb 2000 12:23:08 +0100 | wenzelm | mkdir -p $ISABELLE_BROWSER_INFO; | changeset | files |
| Mon, 14 Feb 2000 11:23:57 +0100 | wenzelm | fixed prefer; | changeset | files |
| Mon, 14 Feb 2000 11:23:44 +0100 | wenzelm | tuned msg; | changeset | files |
| Sun, 13 Feb 2000 21:01:26 +0100 | wenzelm | added refine_end; | changeset | files |
| Sun, 13 Feb 2000 21:00:02 +0100 | wenzelm | tuned attrib; | changeset | files |