Wed, 11 Jul 2007 11:35:17 +0200 aspinall Fix nested PGIP messages. Update for schema simplifications.
Wed, 11 Jul 2007 11:34:38 +0200 berghofe Moved unify_consts to PrimrecPackage.
Wed, 11 Jul 2007 11:32:02 +0200 berghofe - Renamed inductive2 to inductive
Wed, 11 Jul 2007 11:29:44 +0200 berghofe Adapted to changes in Predicate theory.
Wed, 11 Jul 2007 11:28:13 +0200 berghofe Adapted to new inductive definition package.
Wed, 11 Jul 2007 11:27:46 +0200 berghofe Renamed accessible part for predicates to accp.
Wed, 11 Jul 2007 11:25:24 +0200 aspinall Track schema changes: merge messagecategory with area attributes
Wed, 11 Jul 2007 11:25:21 +0200 berghofe bot is now a constant.
Wed, 11 Jul 2007 11:24:36 +0200 berghofe Restored set notation.
Wed, 11 Jul 2007 11:23:24 +0200 berghofe - Renamed inductive2 to inductive
Wed, 11 Jul 2007 11:22:02 +0200 aspinall Track schema changes: remove cleardisplay, proofstate messages. Simplify attributes on cleardisplay, normalresponse.
Wed, 11 Jul 2007 11:21:10 +0200 aspinall Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
Wed, 11 Jul 2007 11:16:34 +0200 berghofe Renamed inductive2 to inductive.
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 11 Jul 2007 11:13:08 +0200 berghofe New operations on tuples with specific arities.
Wed, 11 Jul 2007 11:11:39 +0200 berghofe Adapted to changes in infrastructure for converting between
Wed, 11 Jul 2007 11:10:37 +0200 berghofe rtrancl and trancl are now defined using inductive_set.
Wed, 11 Jul 2007 11:09:15 +0200 berghofe Removed wf_implies_wfP and wfP_implies_wf from list of hints again.
Wed, 11 Jul 2007 11:07:57 +0200 berghofe - Moved infrastructure for converting between sets and predicates
Wed, 11 Jul 2007 11:04:39 +0200 berghofe Adapted to new package for inductive sets.
Wed, 11 Jul 2007 11:03:11 +0200 berghofe Inserted definition of in_rel again (since member2 was removed).
Wed, 11 Jul 2007 11:02:07 +0200 berghofe Added ML bindings for sup_fun_eq and sup_bool_eq.
Wed, 11 Jul 2007 11:01:24 +0200 berghofe top and bot are now constants.
Wed, 11 Jul 2007 11:00:46 +0200 berghofe Renamed inductive2 to inductive.
Wed, 11 Jul 2007 11:00:09 +0200 berghofe acc is now defined using inductive_set.
Wed, 11 Jul 2007 10:59:23 +0200 berghofe Added new package for inductive sets.
Wed, 11 Jul 2007 10:53:39 +0200 berghofe Adapted to new inductive definition package.
Wed, 11 Jul 2007 10:52:20 +0200 berghofe Adapted to changes in inductive definition package.
Wed, 11 Jul 2007 00:46:48 +0200 wenzelm tuned comment markup;
Wed, 11 Jul 2007 00:29:52 +0200 wenzelm treat OuterLex.Error;
Wed, 11 Jul 2007 00:29:51 +0200 wenzelm separated Malformed (symbolic char) from Error (bad input);
Wed, 11 Jul 2007 00:29:50 +0200 wenzelm Output.escape_malformed;
Wed, 11 Jul 2007 00:29:49 +0200 wenzelm added escape_malformed (failsafe);
Tue, 10 Jul 2007 23:29:53 +0200 wenzelm Basic editing of theory sources.
Tue, 10 Jul 2007 23:29:52 +0200 wenzelm tuned;
Tue, 10 Jul 2007 23:29:51 +0200 wenzelm export html_mode, begin_document, end_document;
Tue, 10 Jul 2007 23:29:49 +0200 wenzelm renamed XML.Rawtext to XML.Output;
Tue, 10 Jul 2007 23:29:47 +0200 wenzelm export get_lexicons;
Tue, 10 Jul 2007 23:29:46 +0200 wenzelm added kind_of;
Tue, 10 Jul 2007 23:29:44 +0200 wenzelm Markup.enclose;
Tue, 10 Jul 2007 23:29:43 +0200 wenzelm more markup for inner and outer syntax;
Tue, 10 Jul 2007 23:29:41 +0200 wenzelm simplified funpow, untabify;
Tue, 10 Jul 2007 23:29:38 +0200 wenzelm added Thy/thy_edit.ML;
Tue, 10 Jul 2007 23:29:35 +0200 wenzelm added some markup for outer syntax;
Tue, 10 Jul 2007 17:30:57 +0200 haftmann clarified merge of module names
Tue, 10 Jul 2007 17:30:56 +0200 haftmann now a monolithic module
Tue, 10 Jul 2007 17:30:54 +0200 haftmann now works with SML/NJ
Tue, 10 Jul 2007 17:30:53 +0200 haftmann tuned
Tue, 10 Jul 2007 17:30:52 +0200 haftmann improvement for code names
Tue, 10 Jul 2007 17:30:51 +0200 haftmann removed proof dependency on transitivity theorems
Tue, 10 Jul 2007 17:30:50 +0200 haftmann moved lfp_induct2 here
Tue, 10 Jul 2007 17:30:49 +0200 haftmann clarified import
Tue, 10 Jul 2007 17:30:47 +0200 haftmann moved lfp_induct2 to Relation.thy
Tue, 10 Jul 2007 17:30:45 +0200 haftmann moved some finite lemmas here
Tue, 10 Jul 2007 17:30:43 +0200 haftmann moved finite lemmas to Finite_Set.thy
Tue, 10 Jul 2007 16:46:37 +0200 wenzelm added print_mode setup (from pretty.ML);
Tue, 10 Jul 2007 16:45:06 +0200 wenzelm Markup.add_mode;
Tue, 10 Jul 2007 16:45:05 +0200 wenzelm removed no_state markup -- produce empty state;
Tue, 10 Jul 2007 16:45:04 +0200 wenzelm Markup.output;
Tue, 10 Jul 2007 16:45:03 +0200 wenzelm moved source cascading from scan.ML to source.ML;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip