| Mon, 21 Aug 2000 19:17:07 +0200 | wenzelm | updated; | changeset | files |
| Mon, 21 Aug 2000 19:03:58 +0200 | wenzelm | updated; | changeset | files |
| Mon, 21 Aug 2000 18:49:38 +0200 | wenzelm | tuned translations; | changeset | files |
| Mon, 21 Aug 2000 18:45:29 +0200 | nipkow | *** empty log message *** | changeset | files |
| Mon, 21 Aug 2000 18:40:30 +0200 | wenzelm | added \isastyleminor; | changeset | files |
| Mon, 21 Aug 2000 18:38:27 +0200 | wenzelm | more \isachars; | changeset | files |
| Mon, 21 Aug 2000 18:16:47 +0200 | wenzelm | fixed has_meta_prems: strip_assums_hyp; | changeset | files |
| Mon, 21 Aug 2000 17:54:43 +0200 | nipkow | *** empty log message *** | changeset | files |
| Mon, 21 Aug 2000 13:47:24 +0200 | wenzelm | updated; | changeset | files |
| Sun, 20 Aug 2000 17:45:20 +0200 | wenzelm | open cases; | changeset | files |
| Sat, 19 Aug 2000 12:49:19 +0200 | wenzelm | output \isachar; | changeset | files |
| Sat, 19 Aug 2000 12:48:26 +0200 | wenzelm | cond_add_path; | changeset | files |
| Sat, 19 Aug 2000 12:47:16 +0200 | wenzelm | fixed text; | changeset | files |
| Sat, 19 Aug 2000 12:45:11 +0200 | wenzelm | turned into new-style theory; | changeset | files |
| Sat, 19 Aug 2000 12:44:39 +0200 | wenzelm | tuned; | changeset | files |
| Sat, 19 Aug 2000 12:44:20 +0200 | wenzelm | tuned \isastyle; | changeset | files |
| Sat, 19 Aug 2000 12:43:55 +0200 | wenzelm | added \isachar definitions; | changeset | files |
| Sat, 19 Aug 2000 12:42:52 +0200 | wenzelm | %\urlstyle{rm} | changeset | files |
| Sat, 19 Aug 2000 12:41:41 +0200 | wenzelm | renamed cond_with_path to cond_add_path (add to front); | changeset | files |
| Fri, 18 Aug 2000 18:46:02 +0200 | paulson | X-symbols for ordinal, cardinal, integer arithmetic | changeset | files |
| Fri, 18 Aug 2000 18:11:10 +0200 | wenzelm | fixed RuleCases.make (invert flag); | changeset | files |
| Fri, 18 Aug 2000 18:06:10 +0200 | wenzelm | removed obsolete add_recdef_x; | changeset | files |
| Fri, 18 Aug 2000 17:58:33 +0200 | wenzelm | proper handling of defs; | changeset | files |
| Fri, 18 Aug 2000 17:53:49 +0200 | wenzelm | Main now new-style theory; added Main.ML for compatibility; | changeset | files |
| Fri, 18 Aug 2000 12:34:48 +0200 | paulson | simproc bug fix: only TYPING assumptions are given to the simplifier | changeset | files |
| Fri, 18 Aug 2000 12:34:13 +0200 | paulson | better rules for cancellation of common factors across comparisons | changeset | files |
| Fri, 18 Aug 2000 12:31:20 +0200 | paulson | new example ZF/ex/NatSum | changeset | files |
| Fri, 18 Aug 2000 12:30:41 +0200 | paulson | now allows dest_coeff to fail | changeset | files |
| Fri, 18 Aug 2000 11:14:23 +0200 | nipkow | *** empty log message *** | changeset | files |
| Fri, 18 Aug 2000 10:34:08 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 17 Aug 2000 21:07:25 +0200 | wenzelm | removed obsolete keyword; | changeset | files |
| Thu, 17 Aug 2000 21:06:04 +0200 | wenzelm | fixed indexing; | changeset | files |
| Thu, 17 Aug 2000 18:58:49 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 17 Aug 2000 18:31:12 +0200 | nipkow | installed recdef congs data | changeset | files |
| Thu, 17 Aug 2000 18:30:48 +0200 | nipkow | added map_cong to recdef | changeset | files |
| Thu, 17 Aug 2000 16:23:50 +0200 | wenzelm | removed Lambda/Type.ML; | changeset | files |
| Thu, 17 Aug 2000 12:02:01 +0200 | paulson | better rules for cancellation of common factors across comparisons | changeset | files |
| Thu, 17 Aug 2000 12:01:09 +0200 | paulson | fixed a proof that had stopped working ??? | changeset | files |
| Thu, 17 Aug 2000 12:00:23 +0200 | paulson | tidied & updated proofs, deleting some unused ones | changeset | files |
| Thu, 17 Aug 2000 11:56:47 +0200 | paulson | modified proofs: better rules for cancellation of common factors across comparisons | changeset | files |
| Thu, 17 Aug 2000 11:55:47 +0200 | paulson | better rules for cancellation of common factors across comparisons | changeset | files |
| Thu, 17 Aug 2000 10:42:57 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 17 Aug 2000 10:40:31 +0200 | wenzelm | cases: opaque by default; | changeset | files |
| Thu, 17 Aug 2000 10:39:44 +0200 | wenzelm | renamed 'RS' to 'THEN'; | changeset | files |
| Thu, 17 Aug 2000 10:39:30 +0200 | wenzelm | tuned error handling; | changeset | files |
| Thu, 17 Aug 2000 10:39:12 +0200 | wenzelm | added 'symmetric' attribute; | changeset | files |
| Thu, 17 Aug 2000 10:38:43 +0200 | wenzelm | updated; | changeset | files |
| Thu, 17 Aug 2000 10:38:20 +0200 | wenzelm | sel_upd proc: include 'more' pseudo-field; | changeset | files |
| Thu, 17 Aug 2000 10:37:33 +0200 | wenzelm | renamed 'mk_cases_tac' to 'ind_cases'; | changeset | files |
| Thu, 17 Aug 2000 10:37:04 +0200 | wenzelm | changed 'opaque' option to 'open' (opaque is default); | changeset | files |
| Thu, 17 Aug 2000 10:35:49 +0200 | wenzelm | renamed 'RS' to 'THEN'; | changeset | files |
| Thu, 17 Aug 2000 10:34:52 +0200 | wenzelm | converted to new-style theory; | changeset | files |
| Thu, 17 Aug 2000 10:34:28 +0200 | wenzelm | done; | changeset | files |
| Thu, 17 Aug 2000 10:34:11 +0200 | wenzelm | 'symmetric' attribute; | changeset | files |
| Thu, 17 Aug 2000 10:33:37 +0200 | wenzelm | fixed deps; | changeset | files |
| Thu, 17 Aug 2000 10:33:13 +0200 | wenzelm | renamed 'RS' to 'THEN'; | changeset | files |
| Thu, 17 Aug 2000 10:32:44 +0200 | wenzelm | index tokens; | changeset | files |
| Thu, 17 Aug 2000 10:32:20 +0200 | wenzelm | cases/induct method: 'opaque' by default; added 'open' option; | changeset | files |
| Thu, 17 Aug 2000 10:31:43 +0200 | wenzelm | updated; | changeset | files |
| Thu, 17 Aug 2000 10:31:10 +0200 | wenzelm | renamed 'RS' to 'THEN'; | changeset | files |
| Thu, 17 Aug 2000 10:29:50 +0200 | wenzelm | fixed lbrace, rbrace; | changeset | files |
| Thu, 17 Aug 2000 10:29:23 +0200 | wenzelm | Isar/Pure: renamed 'RS' attribute to 'THEN'; | changeset | files |
| Wed, 16 Aug 2000 18:10:15 +0200 | nipkow | Fixed completeness bug in simplifier: congruence rules could preclude | changeset | files |
| Wed, 16 Aug 2000 10:25:02 +0200 | paulson | major sharpening of stable_project_transient | changeset | files |
| Wed, 16 Aug 2000 10:23:25 +0200 | paulson | new (unused) lemma | changeset | files |
| Wed, 16 Aug 2000 10:22:41 +0200 | paulson | new thm and simprule Compl_Diff_eq | changeset | files |
| Mon, 14 Aug 2000 18:49:35 +0200 | wenzelm | added conversion.tex; | changeset | files |
| Mon, 14 Aug 2000 18:49:23 +0200 | wenzelm | moved tactic emulation methods here; | changeset | files |
| Mon, 14 Aug 2000 18:47:32 +0200 | wenzelm | added 'declare' command; | changeset | files |
| Mon, 14 Aug 2000 18:45:49 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 14 Aug 2000 18:45:31 +0200 | wenzelm | updated; | changeset | files |
| Mon, 14 Aug 2000 18:45:16 +0200 | wenzelm | renamed 'intrs' to 'intros'; | changeset | files |
| Mon, 14 Aug 2000 18:43:57 +0200 | wenzelm | updated command termination issue; | changeset | files |
| Mon, 14 Aug 2000 18:43:30 +0200 | wenzelm | some more refs; | changeset | files |
| Mon, 14 Aug 2000 18:42:57 +0200 | wenzelm | Aspinall:2000:eProof; | changeset | files |
| Mon, 14 Aug 2000 18:14:54 +0200 | wenzelm | raplaced "intrs" by "intrs" (new-style only); | changeset | files |
| Mon, 14 Aug 2000 18:13:42 +0200 | wenzelm | cases: support multiple insts; | changeset | files |
| Mon, 14 Aug 2000 18:13:14 +0200 | wenzelm | intros; | changeset | files |
| Mon, 14 Aug 2000 18:08:26 +0200 | kleing | added MicroJava/BV/StepMono.thy, | changeset | files |
| Mon, 14 Aug 2000 18:03:19 +0200 | kleing | Convert.thy now in Isar, tuned | changeset | files |
| Mon, 14 Aug 2000 14:57:29 +0200 | wenzelm | tuned names; | changeset | files |
| Mon, 14 Aug 2000 14:53:47 +0200 | wenzelm | added hypsubst; | changeset | files |
| Mon, 14 Aug 2000 14:53:26 +0200 | wenzelm | added "fastsimp"; | changeset | files |
| Mon, 14 Aug 2000 14:51:51 +0200 | wenzelm | added declare_theorems(_i); | changeset | files |
| Mon, 14 Aug 2000 14:50:53 +0200 | wenzelm | added "declare" command; | changeset | files |
| Mon, 14 Aug 2000 14:50:32 +0200 | wenzelm | added thy_script kind; | changeset | files |
| Mon, 14 Aug 2000 14:50:11 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 14 Aug 2000 14:49:49 +0200 | wenzelm | use_let: exclude 'val'; | changeset | files |
| Mon, 14 Aug 2000 14:48:07 +0200 | wenzelm | fixed document preparation; | changeset | files |
| Sat, 12 Aug 2000 21:42:51 +0200 | paulson | documented the integers and updated section on nat arithmetic | changeset | files |
| Sat, 12 Aug 2000 21:42:12 +0200 | paulson | some ad-hoc simprules for div and mod to reduce the | changeset | files |
| Sat, 12 Aug 2000 21:41:42 +0200 | paulson | deleted needless rules | changeset | files |
| Fri, 11 Aug 2000 14:53:48 +0200 | kleing | added bind_thm for widen_RefT etc. | changeset | files |
| Fri, 11 Aug 2000 14:52:52 +0200 | kleing | tuned | changeset | files |
| Fri, 11 Aug 2000 14:52:39 +0200 | kleing | added LBV | changeset | files |
| Fri, 11 Aug 2000 13:27:17 +0200 | paulson | new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers | changeset | files |