Mon, 24 Apr 2006 16:37:52 +0200 haftmann seperated typedef codegen from main code
Mon, 24 Apr 2006 16:37:37 +0200 haftmann more precise tactics
Mon, 24 Apr 2006 16:37:07 +0200 haftmann fixed typo
Mon, 24 Apr 2006 16:36:34 +0200 haftmann more precise data structure
Mon, 24 Apr 2006 16:36:07 +0200 haftmann cleaned up some diagnostic mathom
Mon, 24 Apr 2006 16:35:30 +0200 haftmann moved coalesce to AList, added equality predicates to library
Sun, 23 Apr 2006 10:57:48 +0200 obua added LP.thy
Sat, 22 Apr 2006 06:06:39 +0200 mengj Changed the treatment of equalities.
Thu, 20 Apr 2006 04:20:06 +0200 mengj Changed the logic detection method.
Wed, 19 Apr 2006 13:11:35 +0200 paulson exported linkup_logic_mode and changed the default setting
Wed, 19 Apr 2006 10:43:53 +0200 paulson fix to spacing in switches, for Vampire under SML/NJ
Wed, 19 Apr 2006 10:43:09 +0200 paulson definition expansion checks for excess variables
Wed, 19 Apr 2006 10:42:45 +0200 paulson the "th" field of type "clause"
Wed, 19 Apr 2006 10:42:13 +0200 paulson tidying and reformatting
Wed, 19 Apr 2006 10:41:37 +0200 paulson tidying; ATP options including CASC mode for Vampire
Tue, 18 Apr 2006 05:38:18 +0200 mengj Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
Tue, 18 Apr 2006 05:37:43 +0200 mengj Take conjectures and axioms as thms when convert them to ResClause.clause format.
Tue, 18 Apr 2006 05:36:38 +0200 mengj Tidied up some programs.
Sun, 16 Apr 2006 08:22:29 +0200 haftmann fixed typo
Thu, 13 Apr 2006 23:15:44 +0200 huffman add lemma less_UU_iff as default simp rule
Thu, 13 Apr 2006 23:14:18 +0200 huffman hide common name of constant 'run'
Thu, 13 Apr 2006 12:01:16 +0200 wenzelm early test of Classpackage, Codegenerator;
Thu, 13 Apr 2006 12:01:15 +0200 wenzelm fixed typo in method invocation;
Thu, 13 Apr 2006 12:01:14 +0200 wenzelm ignore sort constraints of consts declarations;
Thu, 13 Apr 2006 12:01:13 +0200 wenzelm ignore sort constraints of consts declarations;
Thu, 13 Apr 2006 12:01:12 +0200 wenzelm add_axclass(_i): canonical specification format;
Thu, 13 Apr 2006 12:01:11 +0200 wenzelm certify: ignore sort constraints of declarations (MAJOR CHANGE);
Thu, 13 Apr 2006 12:01:10 +0200 wenzelm added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
Thu, 13 Apr 2006 12:01:09 +0200 wenzelm axclass: old-style concrete syntax for canonical specification format;
Thu, 13 Apr 2006 12:01:08 +0200 wenzelm ProofDisplay.print_theorems/theory;
Thu, 13 Apr 2006 12:01:07 +0200 wenzelm added maxidx_of;
Thu, 13 Apr 2006 12:01:06 +0200 wenzelm tuned;
Thu, 13 Apr 2006 12:01:05 +0200 wenzelm added typ_equiv;
Thu, 13 Apr 2006 12:01:04 +0200 wenzelm moved print_theorems/theory to Isar/proof_display.ML;
Thu, 13 Apr 2006 12:01:03 +0200 wenzelm added dest_conjunction_list;
Thu, 13 Apr 2006 12:01:02 +0200 wenzelm export unflat (again);
Thu, 13 Apr 2006 12:01:01 +0200 wenzelm use conjunction stuff from conjunction.ML;
Thu, 13 Apr 2006 12:01:00 +0200 wenzelm expand_atom: Type.raw_match;
Thu, 13 Apr 2006 12:00:59 +0200 wenzelm added equal_elim_rule2;
Thu, 13 Apr 2006 12:00:58 +0200 wenzelm tuned comment;
Thu, 13 Apr 2006 12:00:56 +0200 wenzelm ignore sorts of consts declarations;
Thu, 13 Apr 2006 12:00:55 +0200 wenzelm reworded add_axclass(_i): canonical specification format,
Thu, 13 Apr 2006 12:00:54 +0200 wenzelm added conjunction.ML;
Thu, 13 Apr 2006 12:00:53 +0200 wenzelm Meta-level conjunction.
Thu, 13 Apr 2006 12:00:51 +0200 wenzelm added conjunction.ML;
Thu, 13 Apr 2006 12:00:50 +0200 wenzelm Sign.typ_equiv;
Thu, 13 Apr 2006 11:22:44 +0200 haftmann added subversion treatment
Tue, 11 Apr 2006 16:00:09 +0200 wenzelm classes: prefer thy operations;
Tue, 11 Apr 2006 16:00:08 +0200 wenzelm export pretty_classrel/arity;
Tue, 11 Apr 2006 16:00:07 +0200 wenzelm 'axclass': no parameters;
Tue, 11 Apr 2006 16:00:06 +0200 wenzelm tuned;
Tue, 11 Apr 2006 16:00:05 +0200 wenzelm removed superclasses (see sign.ML);
Tue, 11 Apr 2006 16:00:03 +0200 wenzelm added super_classes (from sorts.ML);
Tue, 11 Apr 2006 16:00:02 +0200 wenzelm added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
Tue, 11 Apr 2006 16:00:01 +0200 wenzelm moved abstract syntax operations to logic.ML;
Mon, 10 Apr 2006 16:00:34 +0200 obua Moved stuff from Ring_and_Field to Matrix
Mon, 10 Apr 2006 14:37:23 +0200 berghofe Adapted to changed type of add_typedef_i.
Mon, 10 Apr 2006 11:35:02 +0200 nipkow Hoare(Parallel) dependencies on document/*
Mon, 10 Apr 2006 11:34:15 +0200 nipkow added references
Mon, 10 Apr 2006 11:33:36 +0200 nipkow Minimal doc
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip