| 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 |