Thu, 21 Aug 2003 11:41:44 +0200 paulson Change from "tracing" to "warning", as requested by David Aspinall
Wed, 20 Aug 2003 13:34:17 +0200 paulson final tweaks for Isar version
Wed, 20 Aug 2003 13:05:22 +0200 paulson finished conversion to Isar format
Wed, 20 Aug 2003 11:12:48 +0200 paulson new example
Wed, 20 Aug 2003 11:04:17 +0200 paulson new case_tac method
Wed, 20 Aug 2003 11:00:37 +0200 paulson partial conversion to Isar format
Tue, 19 Aug 2003 18:45:48 +0200 paulson partial conversion to Isar format
Tue, 19 Aug 2003 13:54:20 +0200 paulson new case_tac
Tue, 19 Aug 2003 13:53:58 +0200 paulson For the Isar version of the ZF logics manual
Fri, 15 Aug 2003 13:45:39 +0200 paulson converting ex/If to Isar script
Fri, 15 Aug 2003 13:07:01 +0200 paulson A document for UNITY
Wed, 13 Aug 2003 17:44:42 +0200 paulson reformatting change and mention of Introduction to Isabelle
Wed, 13 Aug 2003 17:44:01 +0200 paulson corrections by Viktor Kuncak and minor updating
Wed, 13 Aug 2003 17:24:59 +0200 paulson added tutorial
Wed, 13 Aug 2003 12:28:53 +0200 paulson possibility proof!
Tue, 12 Aug 2003 13:35:03 +0200 paulson ZhouGollmann: new example (fair non-repudiation protocol)
Fri, 08 Aug 2003 15:05:11 +0200 streckem added lemma c_hupd_fst
Fri, 08 Aug 2003 14:59:52 +0200 streckem Modifications after changes in MicroJava/J
Fri, 08 Aug 2003 14:57:46 +0200 streckem Changed lemmas .._type_sound
Fri, 08 Aug 2003 14:54:37 +0200 streckem Added lemma exec_no_xcpt
Thu, 07 Aug 2003 17:46:50 +0200 berghofe test_term now renames variable for size of test data to avoid clashes
Tue, 05 Aug 2003 17:57:39 +0200 nipkow cleaned up
Thu, 31 Jul 2003 14:01:04 +0200 nipkow *** empty log message ***
Thu, 31 Jul 2003 00:01:47 +0200 berghofe Removed extraneous rev in function goal_params (the list of parameters
Tue, 29 Jul 2003 13:32:16 +0200 kleing opened new section for next Isabelle release
Mon, 28 Jul 2003 11:16:38 +0200 berghofe test_term now handles Match exception raised in generated code.
Fri, 25 Jul 2003 17:21:22 +0200 nipkow Replaced \<leadsto> by \<rightharpoonup>
Fri, 25 Jul 2003 10:52:15 +0200 paulson Simplified a proof using presburger
Thu, 24 Jul 2003 18:23:17 +0200 paulson new theory Library/NatPair
Thu, 24 Jul 2003 18:23:00 +0200 paulson declarations moved from PreList.thy
Thu, 24 Jul 2003 17:52:38 +0200 berghofe Fixed two bugs:
Thu, 24 Jul 2003 17:47:56 +0200 berghofe Exported function get_mode.
Thu, 24 Jul 2003 16:41:40 +0200 paulson header comment
Thu, 24 Jul 2003 16:37:04 +0200 paulson new theory NatPair of the injection from nat*nat -> nat
Thu, 24 Jul 2003 16:36:29 +0200 paulson Tidying and replacement of some axioms by specifications
Thu, 24 Jul 2003 16:35:51 +0200 paulson tidied
Tue, 22 Jul 2003 11:05:02 +0200 paulson Added some regression testing for simprocs
Tue, 22 Jul 2003 11:03:42 +0200 paulson fixed simprocs
Mon, 21 Jul 2003 17:27:23 +0200 skalberg Added handling of meta implication and meta quantification.
Mon, 21 Jul 2003 16:19:34 +0200 skalberg Added handling of free variables (provided they are of sort HOL.type).
Mon, 21 Jul 2003 13:02:07 +0200 paulson Tidied some examples
Mon, 21 Jul 2003 10:58:16 +0200 skalberg Added the specification command.
Mon, 21 Jul 2003 08:53:56 +0200 skalberg Changed bstring argument to xstring.
Mon, 21 Jul 2003 08:52:06 +0200 skalberg *** empty log message ***
Sat, 19 Jul 2003 17:35:15 +0200 skalberg Added optional theorem names for the constant definitions added during
Thu, 17 Jul 2003 15:23:20 +0200 skalberg Added package for definition by specification.
Wed, 16 Jul 2003 12:09:41 +0200 paulson tidying
Tue, 15 Jul 2003 15:20:54 +0200 paulson Fixing a simproc bug
Tue, 15 Jul 2003 15:12:22 +0200 paulson tidying
Tue, 15 Jul 2003 08:25:20 +0200 nipkow Some new thm (ex_map_conv?)
Mon, 14 Jul 2003 14:44:06 +0200 kleing use Library.Some/None instead of just Some/None in generated quickcheck code
Fri, 11 Jul 2003 15:01:41 +0200 berghofe Added keywords for random testing.
Fri, 11 Jul 2003 15:00:54 +0200 berghofe Restored old (tail recursive!) version of repeat.
Fri, 11 Jul 2003 15:00:10 +0200 berghofe Exported function goal_params.
Fri, 11 Jul 2003 14:59:50 +0200 berghofe Added several functions for producing random numbers.
Fri, 11 Jul 2003 14:59:11 +0200 berghofe Added functions for random testing.
Fri, 11 Jul 2003 14:57:00 +0200 berghofe Added generator for test case generators.
Fri, 11 Jul 2003 14:56:30 +0200 berghofe mk_int now produces specific constants for 0 and 1.
Fri, 11 Jul 2003 14:55:17 +0200 berghofe - Installed specific code generator for equality enforcing that
Fri, 11 Jul 2003 14:12:41 +0200 oheimb added upd_fst, upd_snd, some thms
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip