| Thu, 27 Jul 2000 18:27:25 +0200 | wenzelm | added theory While; | file | diff | annotate |
| Tue, 25 Jul 2000 00:06:46 +0200 | wenzelm | rearranged setup of arithmetic procedures, avoiding global reference values; | file | diff | annotate |
| Tue, 18 Jul 2000 13:16:48 +0200 | kleing | MicroJava structure changed | file | diff | annotate |
| Sun, 16 Jul 2000 20:49:13 +0200 | wenzelm | added ex/Tuple.thy; | file | diff | annotate |
| Fri, 14 Jul 2000 16:32:51 +0200 | oheimb | re-structuring MicroJava; added Example; corrected := syntax; simplfied cast | file | diff | annotate |
| Fri, 07 Jul 2000 16:46:02 +0200 | oheimb | added IMP/Examples.ML dependence | file | diff | annotate |
| Wed, 05 Jul 2000 17:52:24 +0200 | oheimb | disambiguated := ; added Examples (factorial) | file | diff | annotate |
| Tue, 04 Jul 2000 10:54:46 +0200 | oheimb | disambiguated := ; added Examples (factorial) | file | diff | annotate |
| Wed, 28 Jun 2000 10:37:08 +0200 | paulson | new file Provers/make_elim.ML | file | diff | annotate |
| Fri, 23 Jun 2000 14:00:43 +0200 | berghofe | Added new theory Lambda/Type. | file | diff | annotate |
| Wed, 21 Jun 2000 18:09:09 +0200 | wenzelm | fixed deps; | file | diff | annotate |
| Wed, 07 Jun 2000 12:07:07 +0200 | paulson | Real/simproc.ML now removed | file | diff | annotate |
| Fri, 02 Jun 2000 12:44:04 +0200 | oheimb | added HOL/Prolog | file | diff | annotate |
| Wed, 24 May 2000 18:46:38 +0200 | paulson | Adding SetInterval, deleting UNITY/LessThan | file | diff | annotate |
| Wed, 24 May 2000 12:21:26 +0200 | paulson | restored NatSum.thy | file | diff | annotate |
| Tue, 23 May 2000 18:24:48 +0200 | paulson | IntRingDefs is now redundant | file | diff | annotate |
| Tue, 23 May 2000 12:44:03 +0200 | paulson | theory file NatSum.thy no longer needed | file | diff | annotate |
| Mon, 22 May 2000 16:05:22 +0200 | wenzelm | new Isar version of HOL-AxClasses-Tutorial; | file | diff | annotate |
| Mon, 22 May 2000 12:28:34 +0200 | paulson | new file Induct/MultisetOrder.thy | file | diff | annotate |
| Mon, 15 May 2000 10:33:32 +0200 | paulson | added the dummy theory Integ/NatSimprocs.thy | file | diff | annotate |
| Mon, 08 May 2000 20:59:30 +0200 | wenzelm | moved theory Sexp to Induct examples; | file | diff | annotate |
| Fri, 05 May 2000 22:25:17 +0200 | wenzelm | removed Pure/section_utils.ML; | file | diff | annotate |
| Fri, 05 May 2000 12:51:33 +0200 | nipkow | Added AVL | file | diff | annotate |
| Tue, 02 May 2000 18:40:16 +0200 | paulson | combine_numerals replaces both fold_Suc and combine_coeff | file | diff | annotate |
| Fri, 21 Apr 2000 11:27:28 +0200 | paulson | Provers/Arith/inverse_fold.ML is already obsolete | file | diff | annotate |
| Tue, 18 Apr 2000 15:51:59 +0200 | paulson | new simprocs for numerals of type "nat" | file | diff | annotate |
| Wed, 05 Apr 2000 21:08:24 +0200 | wenzelm | added Isar_examples/NestedDatatype.thy; | file | diff | annotate |
| Fri, 24 Mar 2000 17:28:03 +0100 | wenzelm | added HOL/ex/Multiquote.thy; | file | diff | annotate |
| Thu, 23 Mar 2000 11:27:52 +0100 | wenzelm | ex/Antiquote.thy made new-style theory; | file | diff | annotate |
| Thu, 23 Mar 2000 10:22:08 +0100 | paulson | restored the MESON examples file HOL/ex/mesontest2.ML | file | diff | annotate |
| Fri, 17 Mar 2000 17:12:07 +0100 | wenzelm | fixed dep; | file | diff | annotate |
| Thu, 16 Mar 2000 00:35:27 +0100 | wenzelm | added HOL/PreLIst.thy; | file | diff | annotate |
| Wed, 08 Mar 2000 16:14:12 +0100 | paulson | new theory ex/Factorization | file | diff | annotate |
| Sat, 04 Mar 2000 11:42:12 +0100 | paulson | new theories UNITY/Detects, UNITY/Reachability | file | diff | annotate |
| Fri, 18 Feb 2000 15:37:08 +0100 | paulson | Rename: theory for applying a bijection over states to a UNITY program | file | diff | annotate |
| Fri, 04 Feb 2000 21:45:57 +0100 | wenzelm | added MicroJava/document; | file | diff | annotate |
| Tue, 01 Feb 2000 18:18:09 +0100 | oheimb | added forgotten rules to make IMPP | file | diff | annotate |
| Mon, 31 Jan 2000 18:30:35 +0100 | oheimb | added IMPP to HOL | file | diff | annotate |
| Thu, 20 Jan 2000 17:57:59 +0100 | wenzelm | removed Isar_examples/Minimal; | file | diff | annotate |
| Mon, 10 Jan 2000 16:06:43 +0100 | nipkow | Forgot to "call" MicroJava in makefile. | file | diff | annotate |
| Tue, 07 Dec 1999 12:12:54 +0100 | wenzelm | added Isar_examples/Fibonacci.thy; | file | diff | annotate |
| Tue, 30 Nov 1999 16:51:41 +0100 | paulson | new theory UNITY/ELT | file | diff | annotate |
| Mon, 29 Nov 1999 11:21:44 +0100 | wenzelm | Isar_examples/Minimal.thy; | file | diff | annotate |
| Thu, 25 Nov 1999 12:30:57 +0100 | nipkow | del Method.ML | file | diff | annotate |
| Wed, 17 Nov 1999 15:03:23 +0100 | wenzelm | added Isar_examples/Puzzle.thy; | file | diff | annotate |
| Thu, 11 Nov 1999 12:24:48 +0100 | nipkow | Added MicroJava | file | diff | annotate |
| Thu, 11 Nov 1999 11:29:11 +0100 | wenzelm | clean target; | file | diff | annotate |
| Fri, 05 Nov 1999 12:45:37 +0100 | paulson | Algebra and Polynomial theories, by Clemens Ballarin | file | diff | annotate |
| Sat, 30 Oct 1999 20:39:01 +0200 | wenzelm | fixed deps; | file | diff | annotate |
| Thu, 28 Oct 1999 19:53:24 +0200 | wenzelm | fixed deps; | file | diff | annotate |
| Mon, 25 Oct 1999 19:24:31 +0200 | wenzelm | added Real/HahnBanach/document/root.bib; | file | diff | annotate |
| Fri, 22 Oct 1999 20:14:31 +0200 | wenzelm | HahnBanach update by Gertrud Bauer; | file | diff | annotate |
| Fri, 08 Oct 1999 15:08:47 +0200 | wenzelm | include document; | file | diff | annotate |
| Wed, 06 Oct 1999 18:50:40 +0200 | wenzelm | Isar_examples/W_correct; | file | diff | annotate |
| Mon, 04 Oct 1999 21:43:05 +0200 | wenzelm | removed TFL/sys.sml; | file | diff | annotate |
| Tue, 28 Sep 1999 22:17:05 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 28 Sep 1999 16:37:04 +0200 | nipkow | added BCV. | file | diff | annotate |
| Tue, 28 Sep 1999 15:30:52 +0200 | paulson | new UNITY theory: Project | file | diff | annotate |
| Wed, 22 Sep 1999 21:04:34 +0200 | wenzelm | proper theory setup for Real/ex/BinEx; | file | diff | annotate |
| Fri, 10 Sep 1999 17:28:51 +0200 | wenzelm | The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) | file | diff | annotate |