| Thu, 10 Feb 2000 13:34:38 +0100 | wenzelm | add_judgment; | changeset | files |
| Thu, 10 Feb 2000 11:08:42 +0100 | paulson | new thm and simprule inv_id | changeset | files |
| Thu, 10 Feb 2000 11:03:54 +0100 | paulson | Cambridge-specific modifications | changeset | files |
| Wed, 09 Feb 2000 14:35:23 +0100 | wenzelm | mirror dist page; | changeset | files |
| Wed, 09 Feb 2000 14:12:14 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 09 Feb 2000 14:03:29 +0100 | wenzelm | mirror main page; | changeset | files |
| Wed, 09 Feb 2000 13:43:35 +0100 | kleing | clearer "Obtaining" section | changeset | files |
| Wed, 09 Feb 2000 12:30:25 +0100 | wenzelm | [df]rule methods; | changeset | files |
| Wed, 09 Feb 2000 12:30:04 +0100 | wenzelm | document -c; | changeset | files |
| Wed, 09 Feb 2000 12:29:03 +0100 | wenzelm | eliminated gif dir; | changeset | files |
| Wed, 09 Feb 2000 12:28:44 +0100 | wenzelm | option -c; | changeset | files |
| Wed, 09 Feb 2000 11:45:10 +0100 | paulson | updated the Client example | changeset | files |
| Wed, 09 Feb 2000 11:43:53 +0100 | paulson | tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2 | changeset | files |
| Wed, 09 Feb 2000 11:42:26 +0100 | paulson | new thm order_less_imp_le | changeset | files |
| Tue, 08 Feb 2000 22:28:30 +0100 | wenzelm | (then_)tac: assert_backward; | changeset | files |
| Tue, 08 Feb 2000 20:17:41 +0100 | wenzelm | added -c option (beware!); | changeset | files |
| Tue, 08 Feb 2000 20:14:58 +0100 | wenzelm | rename -p to -P; | changeset | files |
| Tue, 08 Feb 2000 20:14:09 +0100 | wenzelm | added forget_proof; | changeset | files |
| Tue, 08 Feb 2000 20:13:58 +0100 | wenzelm | added K.qed_global; | changeset | files |
| Tue, 08 Feb 2000 20:12:36 +0100 | wenzelm | omit Primes; | changeset | files |
| Mon, 07 Feb 2000 18:42:47 +0100 | wenzelm | (then_)apply: prove -> prove; | changeset | files |
| Mon, 07 Feb 2000 18:40:40 +0100 | wenzelm | assert_no_chain; | changeset | files |
| Mon, 07 Feb 2000 18:40:27 +0100 | wenzelm | refine_no_facts: recover goal_facts; | changeset | files |
| Mon, 07 Feb 2000 18:39:53 +0100 | wenzelm | tuned prefer/defer; | changeset | files |
| Mon, 07 Feb 2000 18:38:51 +0100 | wenzelm | intro/elim/dest attributes: changed ! / !! flags to ? / ??; | changeset | files |
| Mon, 07 Feb 2000 15:28:43 +0100 | oheimb | paper available | changeset | files |
| Mon, 07 Feb 2000 15:14:02 +0100 | paulson | tidied some proofs | changeset | files |
| Sat, 05 Feb 2000 17:31:53 +0100 | kleing | Branch: top elements of stack only need to be convertible (not equal) | changeset | files |
| Sat, 05 Feb 2000 17:06:27 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 05 Feb 2000 16:59:50 +0100 | wenzelm | -I option; | changeset | files |
| Sat, 05 Feb 2000 16:58:58 +0100 | wenzelm | -D PATH: dump generated document sources into PATH; | changeset | files |
| Sat, 05 Feb 2000 16:57:02 +0100 | wenzelm | additional tex dump; | changeset | files |
| Sat, 05 Feb 2000 16:54:27 +0100 | wenzelm | '.' == by this; | changeset | files |
| Fri, 04 Feb 2000 21:53:36 +0100 | wenzelm | misc improvements; | changeset | files |
| Fri, 04 Feb 2000 21:45:57 +0100 | wenzelm | added MicroJava/document; | changeset | files |
| Fri, 04 Feb 2000 21:44:38 +0100 | wenzelm | added old_symbol_source; | changeset | files |
| Fri, 04 Feb 2000 21:44:04 +0100 | wenzelm | Present.old_symbol_source; | changeset | files |
| Fri, 04 Feb 2000 21:43:30 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 04 Feb 2000 21:37:23 +0100 | wenzelm | manually load session; | changeset | files |
| Fri, 04 Feb 2000 21:36:13 +0100 | wenzelm | tuned syms; | changeset | files |
| Fri, 04 Feb 2000 11:36:11 +0100 | paulson | new theorem gcd_add_mult | changeset | files |
| Wed, 02 Feb 2000 20:19:25 +0100 | wenzelm | most_general_varify_tfrees all results; | changeset | files |
| Wed, 02 Feb 2000 13:26:38 +0100 | nipkow | Rduced Class C <= Class D to C <= D. | changeset | files |
| Wed, 02 Feb 2000 12:46:57 +0100 | wenzelm | nat as names; | changeset | files |
| Wed, 02 Feb 2000 12:25:54 +0100 | paulson | expandshort | changeset | files |
| Wed, 02 Feb 2000 12:25:29 +0100 | paulson | new lemma fun_cons_restrict_eq | changeset | files |
| Wed, 02 Feb 2000 11:42:17 +0100 | paulson | new theorems by Sidi O. Ehmety | changeset | files |
| Tue, 01 Feb 2000 18:18:36 +0100 | oheimb | added forgotten definition of make_imp_tac | changeset | files |
| Tue, 01 Feb 2000 18:18:09 +0100 | oheimb | added forgotten rules to make IMPP | changeset | files |
| Tue, 01 Feb 2000 12:26:47 +0100 | wenzelm | eliminated nonascii; | changeset | files |
| Mon, 31 Jan 2000 18:30:35 +0100 | oheimb | added IMPP to HOL | changeset | files |
| Mon, 31 Jan 2000 16:19:51 +0100 | paulson | renamed image_Union_eq -> image_Union | changeset | files |
| Mon, 31 Jan 2000 16:19:14 +0100 | paulson | new theorem vimage_Union | changeset | files |
| Mon, 31 Jan 2000 16:18:42 +0100 | paulson | new theorem rev_ImageI | changeset | files |
| Mon, 31 Jan 2000 16:18:09 +0100 | paulson | various theorems about image and inverse image | changeset | files |
| Mon, 31 Jan 2000 16:13:28 +0100 | paulson | Pi_empty1 is a more general simprule than empty_fun | changeset | files |
| Sun, 30 Jan 2000 13:24:41 +0100 | wenzelm | rm -f *.aux; | changeset | files |
| Sat, 29 Jan 2000 14:22:16 +0100 | wenzelm | simp_all method; | changeset | files |
| Fri, 28 Jan 2000 21:58:39 +0100 | wenzelm | eliminated proof script; | changeset | files |
| Fri, 28 Jan 2000 21:57:15 +0100 | wenzelm | HEADGOAL; | changeset | files |
| Fri, 28 Jan 2000 21:56:55 +0100 | wenzelm | added prefer, defer; | changeset | files |
| Fri, 28 Jan 2000 21:56:37 +0100 | wenzelm | added HEADGOAL; | changeset | files |
| Fri, 28 Jan 2000 21:56:02 +0100 | wenzelm | added defer, prefer; | changeset | files |
| Fri, 28 Jan 2000 21:55:43 +0100 | wenzelm | Drule.instantiate; | changeset | files |
| Fri, 28 Jan 2000 21:55:23 +0100 | wenzelm | cp -r; | changeset | files |
| Fri, 28 Jan 2000 15:26:51 +0100 | wenzelm | -p option; | changeset | files |
| Fri, 28 Jan 2000 15:08:15 +0100 | oheimb | added range_composition (also to simpset) | changeset | files |
| Fri, 28 Jan 2000 14:49:00 +0100 | oheimb | added finite_range_updI, finite_range_map_of, finite_range_map_of_override | changeset | files |
| Fri, 28 Jan 2000 14:42:46 +0100 | wenzelm | mkdir: prepare logic session directory; | changeset | files |
| Fri, 28 Jan 2000 14:09:23 +0100 | oheimb | added full_nat_induct | changeset | files |
| Fri, 28 Jan 2000 14:08:54 +0100 | oheimb | added splitE', also to claset | changeset | files |
| Fri, 28 Jan 2000 14:07:53 +0100 | oheimb | added inj_singleton | changeset | files |
| Fri, 28 Jan 2000 14:07:33 +0100 | oheimb | added finite_range_imageI | changeset | files |
| Fri, 28 Jan 2000 12:12:06 +0100 | wenzelm | replaced FIRSTGOAL by FINDGOAL (backtracking!); | changeset | files |
| Fri, 28 Jan 2000 12:10:47 +0100 | wenzelm | maintain standard rules (beware: classical provers provides another version!); | changeset | files |
| Fri, 28 Jan 2000 12:06:52 +0100 | wenzelm | replaced FIRSTGOAL by FINDGOAL (backtracking!); | changeset | files |
| Fri, 28 Jan 2000 12:04:17 +0100 | wenzelm | tuned sig; | changeset | files |
| Fri, 28 Jan 2000 12:03:59 +0100 | wenzelm | map data; | changeset | files |
| Fri, 28 Jan 2000 11:23:41 +0100 | oheimb | added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED | changeset | files |
| Fri, 28 Jan 2000 11:22:02 +0100 | oheimb | beautified spacing for binders with symbols syntax, analogous to HOL.thy | changeset | files |
| Thu, 27 Jan 2000 15:30:10 +0100 | oheimb | *** empty log message *** | changeset | files |
| Wed, 26 Jan 2000 21:12:40 +0100 | wenzelm | 'name' etc. include 'number'; | changeset | files |
| Wed, 26 Jan 2000 21:10:27 +0100 | wenzelm | 'name' syntax includes numbers; | changeset | files |
| Wed, 26 Jan 2000 11:04:38 +0100 | nipkow | optimized xs[i:=x]!j lemmas. | changeset | files |
| Tue, 25 Jan 2000 22:31:53 +0100 | wenzelm | added map, map_st; | changeset | files |
| Tue, 25 Jan 2000 22:28:48 +0100 | wenzelm | added map; | changeset | files |
| Tue, 25 Jan 2000 20:22:57 +0100 | wenzelm | fallback on PureThy version; | changeset | files |
| Tue, 25 Jan 2000 09:25:43 +0100 | nipkow | replaced f : A funcset B by f``A <= B. | changeset | files |
| Mon, 24 Jan 2000 14:48:11 +0100 | kleing | reflexivity simp rules | changeset | files |
| Fri, 21 Jan 2000 10:45:40 +0100 | paulson | new theorem inj_on_restrict_eq | changeset | files |
| Thu, 20 Jan 2000 17:57:59 +0100 | wenzelm | removed Isar_examples/Minimal; | changeset | files |
| Tue, 18 Jan 2000 11:33:31 +0100 | paulson | fixed many bad line & page breaks | changeset | files |
| Tue, 18 Jan 2000 11:00:10 +0100 | paulson | Documented Thm.instantiate (not normalizing) and Drule.instantiate | changeset | files |
| Mon, 17 Jan 2000 15:56:58 +0100 | wenzelm | www; | changeset | files |
| Mon, 17 Jan 2000 15:51:37 +0100 | kleing | Id line inserted | changeset | files |
| Mon, 17 Jan 2000 15:49:55 +0100 | kleing | changes for the makepage script in Admin | changeset | files |
| Mon, 17 Jan 2000 15:49:32 +0100 | kleing | makes Isabelle main web pages | changeset | files |
| Mon, 17 Jan 2000 15:02:18 +0100 | wenzelm | Contents: suppress comments; | changeset | files |
| Mon, 17 Jan 2000 14:10:32 +0100 | paulson | Thm.instantiate no longer normalizes, but Drule.instantiate does | changeset | files |
| Fri, 14 Jan 2000 12:17:53 +0100 | paulson | still working; a bit of polishing | changeset | files |
| Thu, 13 Jan 2000 17:36:58 +0100 | paulson | new lemmas for Ntree recursor example; more simprules; more lemmas borrowed | changeset | files |
| Thu, 13 Jan 2000 17:36:02 +0100 | paulson | change for new rewriting | changeset | files |
| Thu, 13 Jan 2000 17:34:59 +0100 | paulson | added recursor | changeset | files |
| Thu, 13 Jan 2000 17:34:39 +0100 | paulson | change in add_thmss to suppress warning | changeset | files |
| Thu, 13 Jan 2000 17:31:30 +0100 | paulson | a bit of tidying | changeset | files |
| Thu, 13 Jan 2000 17:30:23 +0100 | paulson | working version, with Alloc now working on the same state space as the whole | changeset | files |
| Thu, 13 Jan 2000 17:29:04 +0100 | paulson | new theorem subset_Compl_self_eq | changeset | files |
| Thu, 13 Jan 2000 15:29:52 +0100 | wenzelm | tuned comment; | changeset | files |
| Wed, 12 Jan 2000 15:58:16 +0100 | nipkow | Move some lemmas to List. | changeset | files |
| Wed, 12 Jan 2000 15:58:01 +0100 | nipkow | More lemmas. | changeset | files |
| Mon, 10 Jan 2000 17:08:41 +0100 | wenzelm | isabellesimple: avoid paragraph; | changeset | files |
| Mon, 10 Jan 2000 16:07:29 +0100 | nipkow | int:nat->int is pushed inwards. | changeset | files |
| Mon, 10 Jan 2000 16:06:43 +0100 | nipkow | Forgot to "call" MicroJava in makefile. | changeset | files |
| Fri, 07 Jan 2000 11:06:03 +0100 | paulson | tidied parentheses | changeset | files |
| Fri, 07 Jan 2000 11:04:15 +0100 | paulson | tidied | changeset | files |
| Fri, 07 Jan 2000 11:00:56 +0100 | paulson | new theorem leadsTo_refl and induction rule leadsTo_induct_pre | changeset | files |
| Fri, 07 Jan 2000 10:57:06 +0100 | paulson | better automation for "slice" | changeset | files |
| Fri, 07 Jan 2000 10:55:35 +0100 | paulson | moved some proofs from UNITY/ELT to UNITY/Project | changeset | files |
| Thu, 06 Jan 2000 16:00:18 +0100 | wenzelm | obtain: renamed 'in' to 'where'; | changeset | files |
| Wed, 05 Jan 2000 20:49:37 +0100 | wenzelm | oops'; | changeset | files |
| Wed, 05 Jan 2000 20:47:14 +0100 | wenzelm | oops; | changeset | files |
| Wed, 05 Jan 2000 18:27:07 +0100 | oheimb | improved symbol for subcls relation | changeset | files |
| Wed, 05 Jan 2000 16:13:05 +0100 | oheimb | simplified definition of appl_methds, removing m_head | changeset | files |
| Wed, 05 Jan 2000 12:02:24 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 05 Jan 2000 12:01:14 +0100 | wenzelm | obtain; | changeset | files |
| Wed, 05 Jan 2000 11:58:18 +0100 | wenzelm | comment: any number of texts; | changeset | files |
| Wed, 05 Jan 2000 11:57:47 +0100 | wenzelm | proof markup: any mode; | changeset | files |
| Wed, 05 Jan 2000 11:56:04 +0100 | wenzelm | replaced HOLogic.termTVar by HOLogic.termT; | changeset | files |
| Wed, 05 Jan 2000 11:50:55 +0100 | wenzelm | ObtainFun; | changeset | files |
| Wed, 05 Jan 2000 11:50:13 +0100 | wenzelm | METHOD_CLASET': refer to *local* claset; | changeset | files |
| Wed, 05 Jan 2000 11:48:08 +0100 | wenzelm | moved obtain to obtain.ML; | changeset | files |
| Wed, 05 Jan 2000 11:47:46 +0100 | wenzelm | TypeInfer.logicT; | changeset | files |
| Wed, 05 Jan 2000 11:45:31 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 05 Jan 2000 11:45:01 +0100 | wenzelm | ObtainFun; | changeset | files |
| Wed, 05 Jan 2000 11:43:37 +0100 | wenzelm | added thms_ctxt_args; | changeset | files |
| Wed, 05 Jan 2000 11:43:09 +0100 | wenzelm | prepare patterns only once; | changeset | files |
| Wed, 05 Jan 2000 11:42:02 +0100 | wenzelm | ObtainFun; | changeset | files |
| Wed, 05 Jan 2000 11:41:38 +0100 | wenzelm | present chapter; | changeset | files |
| Wed, 05 Jan 2000 11:40:13 +0100 | wenzelm | removed pats; | changeset | files |
| Wed, 05 Jan 2000 11:38:48 +0100 | wenzelm | chapter; | changeset | files |
| Wed, 05 Jan 2000 11:37:44 +0100 | wenzelm | support for dummy variables (anyT, logicT); | changeset | files |
| Wed, 05 Jan 2000 11:35:18 +0100 | wenzelm | TypeInfer.logicT; | changeset | files |
| Tue, 04 Jan 2000 17:05:43 +0100 | oheimb | new arg type for max_spec etc. | changeset | files |
| Mon, 03 Jan 2000 17:33:34 +0100 | bauerg | small changes; | changeset | files |
| Mon, 03 Jan 2000 14:07:10 +0100 | oheimb | removed inj_eq from the default simpset again | changeset | files |
| Mon, 03 Jan 2000 14:07:08 +0100 | oheimb | removed inj_eq from the default simpset again | changeset | files |
| Thu, 23 Dec 1999 19:59:50 +0100 | oheimb | removed inj_eq from the default simpset again | changeset | files |
| Thu, 23 Dec 1999 16:55:27 +0100 | kleing | updated sml package name in installation exmaple | changeset | files |
| Wed, 22 Dec 1999 20:29:59 +0100 | wenzelm | raw_t(e)xt: any proof mode; | changeset | files |
| Wed, 22 Dec 1999 20:29:36 +0100 | wenzelm | fixed error msg; | changeset | files |
| Wed, 22 Dec 1999 20:29:19 +0100 | wenzelm | marg_comment: repeat; | changeset | files |
| Wed, 22 Dec 1999 20:28:56 +0100 | wenzelm | text: string list; | changeset | files |
| Wed, 22 Dec 1999 17:20:01 +0100 | paulson | tidied, with a bit more progress | changeset | files |
| Wed, 22 Dec 1999 17:18:03 +0100 | paulson | Working version after a FAILED attempt to base Follows upon LeadsETo | changeset | files |
| Wed, 22 Dec 1999 17:16:53 +0100 | paulson | new weakening laws | changeset | files |
| Wed, 22 Dec 1999 17:16:23 +0100 | paulson | removing the "{} : CC" requirement for leadsTo[CC] | changeset | files |
| Wed, 22 Dec 1999 16:13:29 +0100 | kleing | back to old sml version (due to c library problems) | changeset | files |
| Wed, 22 Dec 1999 16:12:38 +0100 | kleing | some tuning (incorporated David's suggestions) | changeset | files |
| Tue, 21 Dec 1999 15:03:02 +0100 | paulson | working with weak LeadsTo in guarantees precondition\! | changeset | files |
| Tue, 21 Dec 1999 11:27:32 +0100 | oheimb | corrected, improved eMail addresses, user interface section | changeset | files |
| Fri, 17 Dec 1999 10:30:48 +0100 | paulson | now workign as far as System_Alloc_Progress | changeset | files |
| Thu, 16 Dec 1999 17:01:16 +0100 | paulson | SOUNDNESS BUG FIX for rotate_rule. The original code did not expect | changeset | files |
| Wed, 15 Dec 1999 10:45:37 +0100 | paulson | first working version to Alloc/System_Client_Progress; | changeset | files |
| Mon, 13 Dec 1999 10:54:04 +0100 | paulson | expandshort | changeset | files |
| Thu, 09 Dec 1999 18:33:39 +0100 | kleing | dist page now in page/dist-{content|layout} | changeset | files |
| Thu, 09 Dec 1999 13:35:01 +0100 | wenzelm | updated; | changeset | files |
| Thu, 09 Dec 1999 13:14:27 +0100 | kleing | prettyfied | changeset | files |
| Thu, 09 Dec 1999 13:11:12 +0100 | kleing | full url to local (munich) page | changeset | files |
| Thu, 09 Dec 1999 13:10:39 +0100 | kleing | new web pages integrated | changeset | files |
| Thu, 09 Dec 1999 12:12:45 +0100 | kleing | used for new weg page layout | changeset | files |
| Thu, 09 Dec 1999 11:40:00 +0100 | kleing | ID line added | changeset | files |
| Thu, 09 Dec 1999 11:34:32 +0100 | kleing | new webpage layout | changeset | files |
| Wed, 08 Dec 1999 13:53:29 +0100 | paulson | abolition of localTo: instead "guarantees" has local vars as extra argument | changeset | files |
| Wed, 08 Dec 1999 13:52:36 +0100 | paulson | used image_eq_UN to speed up slow proofs of base cases | changeset | files |
| Wed, 08 Dec 1999 13:51:44 +0100 | paulson | useful lemma eqset_imp_iff | changeset | files |
| Tue, 07 Dec 1999 17:14:49 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 07 Dec 1999 12:13:09 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 07 Dec 1999 12:12:54 +0100 | wenzelm | added Isar_examples/Fibonacci.thy; | changeset | files |
| Tue, 07 Dec 1999 11:01:48 +0100 | nipkow | Fixed bug in find-functions: list of parameters must be reversed before | changeset | files |
| Mon, 06 Dec 1999 14:23:45 +0100 | nipkow | Renamed some vars | changeset | files |
| Thu, 02 Dec 1999 09:09:30 +0100 | nipkow | cosmetic mod. | changeset | files |
| Wed, 01 Dec 1999 22:38:35 +0100 | wenzelm | accommodate current version of rpm; | changeset | files |
| Wed, 01 Dec 1999 18:22:28 +0100 | nipkow | Fixed a problem with returning from the last frame. | changeset | files |
| Wed, 01 Dec 1999 11:20:24 +0100 | paulson | new generalized leads-to theory | changeset | files |
| Wed, 01 Dec 1999 11:15:56 +0100 | paulson | fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER | changeset | files |
| Tue, 30 Nov 1999 17:53:34 +0100 | paulson | deleted rogue copy of localTo_imp_o_localTo | changeset | files |
| Tue, 30 Nov 1999 16:54:10 +0100 | paulson | working version with new theory ELT | changeset | files |
| Tue, 30 Nov 1999 16:51:41 +0100 | paulson | new theory UNITY/ELT | changeset | files |
| Mon, 29 Nov 1999 15:52:49 +0100 | wenzelm | Goal: tuned pris; | changeset | files |
| Mon, 29 Nov 1999 14:12:53 +0100 | nipkow | Removed !! | changeset | files |
| Mon, 29 Nov 1999 11:21:50 +0100 | wenzelm | Minimal.thy; | changeset | files |
| Mon, 29 Nov 1999 11:21:44 +0100 | wenzelm | Isar_examples/Minimal.thy; | changeset | files |
| Mon, 29 Nov 1999 11:21:30 +0100 | wenzelm | qed ""; | changeset | files |
| Fri, 26 Nov 1999 08:46:59 +0100 | nipkow | Various little changes like cmethd -> method and cfield -> field. | changeset | files |
| Thu, 25 Nov 1999 12:30:57 +0100 | nipkow | del Method.ML | changeset | files |
| Thu, 25 Nov 1999 12:01:28 +0100 | nipkow | Minor mods. | changeset | files |
| Wed, 24 Nov 1999 13:36:14 +0100 | wenzelm | renamed comp to compile (avoids clash with Relation.comp); | changeset | files |
| Wed, 24 Nov 1999 13:35:31 +0100 | wenzelm | prove_goal thy; | changeset | files |
| Wed, 24 Nov 1999 12:12:36 +0100 | nipkow | Basis now Main. | changeset | files |
| Wed, 24 Nov 1999 10:25:28 +0100 | paulson | tidied, choosing nicer names | changeset | files |
| Tue, 23 Nov 1999 11:19:39 +0100 | paulson | distributive laws for * over - | changeset | files |
| Tue, 23 Nov 1999 11:18:42 +0100 | paulson | tidied | changeset | files |
| Tue, 23 Nov 1999 11:18:19 +0100 | paulson | new theorem rev_image_eqI | changeset | files |
| Mon, 22 Nov 1999 12:10:27 +0100 | nipkow | Added linord_less_split | changeset | files |
| Fri, 19 Nov 1999 16:30:52 +0100 | oheimb | re-shaped and re-ordered conversion relations | changeset | files |
| Thu, 18 Nov 1999 12:12:39 +0100 | nipkow | Streamlined it a bit more. | changeset | files |
| Thu, 18 Nov 1999 08:50:19 +0100 | nipkow | A small mod. | changeset | files |
| Wed, 17 Nov 1999 15:03:23 +0100 | wenzelm | added Isar_examples/Puzzle.thy; | changeset | files |
| Wed, 17 Nov 1999 11:16:26 +0100 | paulson | tidied | changeset | files |
| Mon, 15 Nov 1999 09:41:06 +0100 | nipkow | Streamlined it a bit. | changeset | files |
| Fri, 12 Nov 1999 18:16:48 +0100 | oheimb | removed full_SetCompr_eq from simpset() again | changeset | files |
| Fri, 12 Nov 1999 17:45:36 +0100 | nipkow | Added the proof by Nielson & Nielson. | changeset | files |
| Fri, 12 Nov 1999 10:57:28 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 11 Nov 1999 16:14:50 +0100 | paulson | HOL changes | changeset | files |
| Thu, 11 Nov 1999 12:44:08 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 11 Nov 1999 12:24:48 +0100 | nipkow | Added MicroJava | changeset | files |
| Thu, 11 Nov 1999 12:23:45 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 11 Nov 1999 11:58:51 +0100 | wenzelm | with_path; | changeset | files |
| Thu, 11 Nov 1999 11:43:14 +0100 | nipkow | Imported Conny's lemmas from MicroJava | changeset | files |
| Thu, 11 Nov 1999 11:29:11 +0100 | wenzelm | clean target; | changeset | files |
| Thu, 11 Nov 1999 11:27:31 +0100 | wenzelm | header; | changeset | files |
| Thu, 11 Nov 1999 10:25:29 +0100 | paulson | tidied | changeset | files |
| Thu, 11 Nov 1999 10:25:17 +0100 | paulson | new-style infix declaration for "image" | changeset | files |
| Thu, 11 Nov 1999 10:24:14 +0100 | paulson | Fixed obsolete use of "op ^^"; new lemma | changeset | files |