Mon, 02 Nov 2009 20:50:48 +0100 |
wenzelm |
modernized structure Proof_Syntax;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 23:48:56 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 22:56:14 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
Wed, 25 Mar 2009 16:54:49 +0100 |
wenzelm |
Proofterm.approximate_proof_body;
|
file |
diff |
annotate
|
Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 15:42:19 +0100 |
wenzelm |
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
Tue, 27 Jan 2009 00:29:37 +0100 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
Sun, 16 Nov 2008 18:18:45 +0100 |
berghofe |
Frees in PThms are now quantified in the order of their appearance in the
|
file |
diff |
annotate
|
Sat, 15 Nov 2008 21:31:27 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
file |
diff |
annotate
|
Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 18:54:59 +0200 |
wenzelm |
OldGoals.simple_read_term;
|
file |
diff |
annotate
|
Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 19:14:03 +0100 |
wenzelm |
simplified PureThy.store_thm;
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
Thu, 20 Mar 2008 00:20:44 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
Sun, 11 Nov 2007 14:00:08 +0100 |
wenzelm |
renamed Symtab.update_list to Symtab.cons_list;
|
file |
diff |
annotate
|
Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
Thu, 10 May 2007 15:50:56 +0200 |
berghofe |
Adapted to new naming scheme for definitions.
|
file |
diff |
annotate
|
Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
Fri, 20 Apr 2007 11:21:53 +0200 |
haftmann |
adds extracted program to code theorem table
|
file |
diff |
annotate
|
Mon, 16 Apr 2007 16:11:03 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
Fri, 13 Apr 2007 16:40:16 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
Mon, 09 Oct 2006 02:19:49 +0200 |
wenzelm |
attribute: Context.mapping;
|
file |
diff |
annotate
|
Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
Tue, 25 Apr 2006 22:23:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 10 Apr 2006 00:33:49 +0200 |
wenzelm |
Term.itselfT;
|
file |
diff |
annotate
|
Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
Mon, 06 Feb 2006 20:59:56 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
Mon, 06 Feb 2006 11:01:28 +0100 |
haftmann |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
file |
diff |
annotate
|
Fri, 03 Feb 2006 23:12:28 +0100 |
wenzelm |
canonical member/insert/merge;
|
file |
diff |
annotate
|
Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some new-style AList operations
|
file |
diff |
annotate
|
Fri, 02 Sep 2005 15:54:47 +0200 |
haftmann |
some 'assoc' etc. refactoring
|
file |
diff |
annotate
|
Thu, 01 Sep 2005 22:15:10 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
file |
diff |
annotate
|
Mon, 01 Aug 2005 19:20:37 +0200 |
wenzelm |
replaced atless by term_ord;
|
file |
diff |
annotate
|
Fri, 15 Jul 2005 15:44:20 +0200 |
wenzelm |
tuned fold on terms;
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 16:07:21 +0200 |
wenzelm |
improved Net interface;
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 11:30:37 +0200 |
haftmann |
(fix for an accidental commit)
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 11:16:34 +0200 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
Mon, 20 Jun 2005 22:13:59 +0200 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
Sat, 11 Jun 2005 22:15:47 +0200 |
wenzelm |
renamed Sign.intern_tycon to Sign.intern_type;
|
file |
diff |
annotate
|
Thu, 09 Jun 2005 12:03:36 +0200 |
wenzelm |
can (Thm.get_axiom_i thy) name;
|
file |
diff |
annotate
|
Sun, 05 Jun 2005 23:07:25 +0200 |
wenzelm |
Type.freeze;
|
file |
diff |
annotate
|
Thu, 02 Jun 2005 18:29:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 31 May 2005 11:53:40 +0200 |
wenzelm |
Theory.restore_naming;
|
file |
diff |
annotate
|
Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
Thu, 21 Apr 2005 19:13:03 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
Mon, 24 Jan 2005 17:59:48 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
Fri, 10 Dec 2004 16:57:01 +0100 |
berghofe |
Added term cache to function condrew in order to speed up rewriting.
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Tue, 01 Jun 2004 12:33:50 +0200 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
Fri, 19 Mar 2004 10:42:38 +0100 |
paulson |
Removing the datatype declaration of "order" allows the standard General.order
|
file |
diff |
annotate
|
Wed, 29 Jan 2003 17:32:01 +0100 |
berghofe |
Fixed bug in function corr.
|
file |
diff |
annotate
|
Wed, 27 Nov 2002 17:23:19 +0100 |
berghofe |
Correctness proofs are now modular, too.
|
file |
diff |
annotate
|
Sun, 17 Nov 2002 23:43:53 +0100 |
berghofe |
Fixed small bug that caused some definitions to be "forgotten".
|
file |
diff |
annotate
|
Wed, 13 Nov 2002 15:36:06 +0100 |
berghofe |
- exported functions etype_of and mk_typ
|
file |
diff |
annotate
|
Mon, 30 Sep 2002 16:42:46 +0200 |
berghofe |
Added check for axioms with "realizes Null A = A".
|
file |
diff |
annotate
|
Wed, 24 Jul 2002 16:16:44 +0200 |
berghofe |
Tuned type constraint of function merge_rules to make smlnj happy.
|
file |
diff |
annotate
|
Sun, 21 Jul 2002 15:37:04 +0200 |
berghofe |
Added program extraction module.
|
file |
diff |
annotate
|