| Mon, 18 Jul 2011 23:48:28 +0200 |
killed use of PolyML.makestring
|
file | diff | annotate |
| Wed, 13 Jul 2011 00:23:24 +0900 |
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
|
file | diff | annotate |
| Thu, 09 Jun 2011 23:12:02 +0200 |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file | diff | annotate |
| Sat, 16 Apr 2011 18:11:20 +0200 |
eliminated old List.nth;
|
file | diff | annotate |
| Fri, 08 Apr 2011 16:34:14 +0200 |
discontinued special treatment of structure Lexicon;
|
file | diff | annotate |
| Fri, 08 Apr 2011 15:02:11 +0200 |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
|
file | diff | annotate |
| Fri, 08 Apr 2011 14:20:57 +0200 |
discontinued special treatment of structure Mixfix;
|
file | diff | annotate |
| Mon, 10 Jan 2011 15:45:46 +0100 |
eliminated Int.toString;
|
file | diff | annotate |
| Wed, 01 Dec 2010 13:09:08 +0100 |
just one Term.dest_funT;
|
file | diff | annotate |
| Sat, 20 Nov 2010 00:53:26 +0100 |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file | diff | annotate |
| Mon, 20 Sep 2010 16:05:25 +0200 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| Sun, 12 Sep 2010 19:04:02 +0200 |
eliminated aliases of Type.constraint;
|
file | diff | annotate |
| Thu, 09 Sep 2010 18:17:34 +0200 |
avoid handling interrupts in user code;
|
file | diff | annotate |
| Mon, 06 Sep 2010 19:13:10 +0200 |
more antiquotations;
|
file | diff | annotate |
| Sun, 05 Sep 2010 23:16:21 +0200 |
turned show_brackets into proper configuration option;
|
file | diff | annotate |
| Sun, 05 Sep 2010 21:41:24 +0200 |
turned show_sorts/show_types into proper configuration options;
|
file | diff | annotate |
| Fri, 03 Sep 2010 22:36:16 +0200 |
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
|
file | diff | annotate |
| Fri, 03 Sep 2010 17:43:44 +0200 |
turned show_all_types into proper configuration option;
|
file | diff | annotate |
| Sat, 28 Aug 2010 16:14:32 +0200 |
formerly unnamed infix equality now named HOL.eq
|
file | diff | annotate |
| Fri, 27 Aug 2010 10:56:46 +0200 |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file | diff | annotate |
| Thu, 26 Aug 2010 20:51:17 +0200 |
formerly unnamed infix impliciation now named HOL.implies
|
file | diff | annotate |
| Thu, 19 Aug 2010 16:08:54 +0200 |
more antiquotations
|
file | diff | annotate |
| Thu, 19 Aug 2010 12:11:57 +0200 |
use HOLogic.boolT and @{typ bool} more pervasively
|
file | diff | annotate |
| Thu, 19 Aug 2010 11:02:14 +0200 |
use antiquotations for remaining unqualified constants in HOL
|
file | diff | annotate |
| Tue, 20 Jul 2010 23:09:49 +0200 |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
file | diff | annotate |
| Mon, 12 Jul 2010 20:21:39 +0200 |
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
|
file | diff | annotate |
| Thu, 01 Jul 2010 16:54:42 +0200 |
qualified constants Set.member and Set.Collect
|
file | diff | annotate |
| Fri, 11 Jun 2010 17:14:01 +0200 |
avoid references to old constdefs
|
file | diff | annotate |
| Thu, 27 May 2010 18:10:37 +0200 |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| Thu, 27 May 2010 17:41:27 +0200 |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| Mon, 17 May 2010 23:54:15 +0200 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file | diff | annotate |
| Sat, 15 May 2010 21:50:05 +0200 |
less pervasive names from structure Thm;
|
file | diff | annotate |
| Wed, 05 May 2010 18:25:34 +0200 |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file | diff | annotate |
| Mon, 03 May 2010 16:26:47 +0200 |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file | diff | annotate |
| Mon, 03 May 2010 14:25:56 +0200 |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file | diff | annotate |
| Thu, 29 Apr 2010 22:56:32 +0200 |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file | diff | annotate |
| Sat, 27 Mar 2010 21:38:38 +0100 |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file | diff | annotate |
| Sat, 20 Mar 2010 17:33:11 +0100 |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file | diff | annotate |
| Fri, 19 Mar 2010 00:47:23 +0100 |
typedef etc.: no constraints;
|
file | diff | annotate |
| Sat, 13 Mar 2010 14:43:04 +0100 |
global typedef;
|
file | diff | annotate |
| Fri, 26 Feb 2010 23:05:47 +0100 |
use simplified Syntax.escape;
|
file | diff | annotate |
| Fri, 19 Feb 2010 16:11:45 +0100 |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file | diff | annotate |
| Thu, 29 Oct 2009 23:56:33 +0100 |
eliminated some old folds;
|
file | diff | annotate |
| Wed, 21 Oct 2009 08:16:25 +0200 |
merged
|
file | diff | annotate |
| Wed, 21 Oct 2009 08:14:38 +0200 |
dropped redundant gen_ prefix
|
file | diff | annotate |
| Tue, 20 Oct 2009 16:13:01 +0200 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
| Wed, 21 Oct 2009 00:36:12 +0200 |
standardized basic operations on type option;
|
file | diff | annotate |
| Sat, 17 Oct 2009 15:57:51 +0200 |
indicate CRITICAL nature of various setmp combinators;
|
file | diff | annotate |
| Thu, 15 Oct 2009 23:10:35 +0200 |
space_implode;
|
file | diff | annotate |
| Thu, 15 Oct 2009 16:15:22 +0200 |
sort_strings (cf. Pure/library.ML);
|
file | diff | annotate |
| Tue, 29 Sep 2009 16:24:36 +0200 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| Fri, 28 Aug 2009 21:04:03 +0200 |
modernized messages -- eliminated ctyp/cterm operations;
|
file | diff | annotate |
| Fri, 24 Jul 2009 22:31:27 +0200 |
ML_Context.the_local_context;
|
file | diff | annotate |
| Fri, 24 Jul 2009 21:02:34 +0200 |
explicit OldGoals;
|
file | diff | annotate |
| Tue, 21 Jul 2009 01:03:18 +0200 |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file | diff | annotate |
| Mon, 06 Jul 2009 21:24:30 +0200 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| Fri, 19 Jun 2009 17:23:21 +0200 |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file | diff | annotate |
| Wed, 11 Mar 2009 15:56:49 +0100 |
stripped dead code
|
file | diff | annotate |
| Sat, 07 Mar 2009 23:30:58 +0100 |
minimal adaptions for abstract binding type;
|
file | diff | annotate |
| Sun, 01 Mar 2009 23:36:12 +0100 |
use long names for old-style fold combinators;
|
file | diff | annotate |