Sat, 10 Nov 2007 23:03:52 +0100 wenzelm tuned specifications of 'notation';
Sat, 10 Nov 2007 18:36:10 +0100 wenzelm removed LocalTheory.target_naming/name;
Sat, 10 Nov 2007 18:36:08 +0100 wenzelm put_inductives: be permissive about multiple versions
Sat, 10 Nov 2007 18:36:07 +0100 wenzelm tuned proofs;
Sat, 10 Nov 2007 18:36:06 +0100 wenzelm tuned document;
Sat, 10 Nov 2007 18:36:06 +0100 wenzelm Orderings.min/max: no need to qualify consts;
Sat, 10 Nov 2007 15:58:18 +0100 wenzelm auto_quickcheck ref: set default in ProofGeneral/preferences only
Sat, 10 Nov 2007 15:58:18 +0100 wenzelm ProofGeneral/preferences: auto_quickcheck=true;
Sat, 10 Nov 2007 14:36:33 +0100 wenzelm qualified Proofterm.proofs;
Sat, 10 Nov 2007 14:31:23 +0100 wenzelm @{const}: improved ProofContext.read_const does the job;
Sat, 10 Nov 2007 14:31:22 +0100 wenzelm locale_const: suppress in class body as well (prevents qualified printing);
Sat, 10 Nov 2007 14:31:21 +0100 wenzelm notation: improved ProofContext.read_const does the job;
Sat, 10 Nov 2007 14:31:20 +0100 wenzelm updated;
Sat, 10 Nov 2007 14:31:18 +0100 wenzelm replaced @{const} (allows name only) by proper @{term};
Fri, 09 Nov 2007 23:24:31 +0100 haftmann proper implementation of check phase; non-qualified names for class operations
Fri, 09 Nov 2007 23:24:30 +0100 haftmann explicit message for failed autoquickcheck
Fri, 09 Nov 2007 19:37:35 +0100 wenzelm tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
Fri, 09 Nov 2007 19:37:35 +0100 wenzelm avoid obsolete Sign.read_prop;
Fri, 09 Nov 2007 19:37:33 +0100 wenzelm tuned proofs -- avoid implicit prems;
Fri, 09 Nov 2007 19:37:32 +0100 wenzelm fixed imports path;
Fri, 09 Nov 2007 19:37:30 +0100 wenzelm tuned proofs -- avoid open cases;
Fri, 09 Nov 2007 18:59:56 +0100 krauss function package: using the names of the equations as case names turned out to be impractical => disabled
Fri, 09 Nov 2007 13:41:27 +0100 krauss avoid name clashes when generating code for union, inter
Thu, 08 Nov 2007 22:57:45 +0100 wenzelm oops -- avoid vacous goal message;
Thu, 08 Nov 2007 22:36:46 +0100 wenzelm tuned messages;
Thu, 08 Nov 2007 22:19:43 +0100 wenzelm avoid "import" as identifier, which is a keyword in Alice;
Thu, 08 Nov 2007 20:52:27 +0100 wenzelm tuned presentation;
Thu, 08 Nov 2007 20:09:17 +0100 wenzelm avoid implicit use of prems;
Thu, 08 Nov 2007 20:08:11 +0100 wenzelm where/of: do not allow schematic variables here!
Thu, 08 Nov 2007 20:08:09 +0100 wenzelm removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
Thu, 08 Nov 2007 20:08:07 +0100 wenzelm discontinued legacy vars;
Thu, 08 Nov 2007 20:08:02 +0100 wenzelm removed unused read_def_terms';
Thu, 08 Nov 2007 20:08:01 +0100 wenzelm eliminated illegal schematic variables in where/of;
Thu, 08 Nov 2007 20:08:00 +0100 wenzelm eliminated illegal schematic variables in where/of;
Thu, 08 Nov 2007 20:07:58 +0100 wenzelm x86_64: fall back on x86 (more efficient);
Thu, 08 Nov 2007 20:07:57 +0100 wenzelm tuned comments;
Thu, 08 Nov 2007 14:51:31 +0100 wenzelm renamed ProofContext.read_const' to ProofContext.read_const_proper;
Thu, 08 Nov 2007 14:51:30 +0100 wenzelm renamed ProofContext.read_const' to ProofContext.read_const_proper;
Thu, 08 Nov 2007 14:51:29 +0100 wenzelm synchronize_syntax: improved declare_const (still inactive);
Thu, 08 Nov 2007 14:51:28 +0100 wenzelm added const_proper;
Thu, 08 Nov 2007 13:24:03 +0100 nipkow added evaluation
Thu, 08 Nov 2007 13:23:47 +0100 nipkow fix
Thu, 08 Nov 2007 13:23:36 +0100 nipkow new general syntax
Thu, 08 Nov 2007 13:23:19 +0100 nipkow tuned
Thu, 08 Nov 2007 13:23:04 +0100 nipkow updated to notation and abbreviation
Thu, 08 Nov 2007 13:21:15 +0100 haftmann added purify_sym
Thu, 08 Nov 2007 13:21:14 +0100 haftmann tuned
Thu, 08 Nov 2007 13:21:12 +0100 haftmann duv, mod, int conversion
Wed, 07 Nov 2007 22:20:13 +0100 wenzelm ProofContext.read_const';
Wed, 07 Nov 2007 22:20:12 +0100 wenzelm Syntax.read_typ;
Wed, 07 Nov 2007 22:20:11 +0100 wenzelm export read_const';
Wed, 07 Nov 2007 22:20:09 +0100 wenzelm Syntax.read_typ;
Wed, 07 Nov 2007 18:19:04 +0100 nipkow added inductive
Wed, 07 Nov 2007 16:43:01 +0100 wenzelm attribute where/of: proper Syntax.parse/check;
Wed, 07 Nov 2007 16:43:00 +0100 wenzelm discontinued ProofContext.read_prop_legacy;
Wed, 07 Nov 2007 16:42:59 +0100 wenzelm discontinued ProofContext.read_prop_legacy;
Wed, 07 Nov 2007 16:42:58 +0100 wenzelm refined Variable.declare_const;
Wed, 07 Nov 2007 16:42:57 +0100 wenzelm refined notion of consts within the local scope;
Wed, 07 Nov 2007 16:42:56 +0100 wenzelm tuned signature;
Wed, 07 Nov 2007 16:42:55 +0100 wenzelm removed obsolete Sign.read_tyname/const (cf. ProofContext);
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip