#
e534c034 |
|
10-Oct-2019 |
wenzelm <none@none> |
unused;
|
#
fc7b6d83 |
|
09-Oct-2019 |
wenzelm <none@none> |
clarified signature -- some operations to support fully explicit proof terms;
|
#
06678ec0 |
|
29-Jul-2019 |
wenzelm <none@none> |
proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
|
#
54e159a9 |
|
29-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
#
24be7acc |
|
29-Jul-2019 |
wenzelm <none@none> |
clarified signature; tuned;
|
#
752574b8 |
|
29-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
#
d08fb3a5 |
|
19-Jul-2019 |
wenzelm <none@none> |
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
|
#
f28683eb |
|
20-Sep-2018 |
wenzelm <none@none> |
clarified standardization of variables, with proper treatment of local variables; tuned signature; tuned;
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
490963f3 |
|
27-Apr-2016 |
wenzelm <none@none> |
tuned;
|
#
d10439ab |
|
26-Apr-2016 |
wenzelm <none@none> |
defs are closed, which leads to proper auto_bind_facts; misc tuning;
|
#
4dcab494 |
|
13-Nov-2015 |
wenzelm <none@none> |
avoid vacuous quantification, as usual for shared variable scope;
|
#
a5a7379a |
|
13-Nov-2015 |
wenzelm <none@none> |
support for structure statements in 'assume', 'presume';
|
#
6f79a399 |
|
09-Jul-2015 |
wenzelm <none@none> |
tuned whitespace;
|
#
2cc93773 |
|
13-Jun-2015 |
wenzelm <none@none> |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
#
54f4e638 |
|
23-Mar-2015 |
wenzelm <none@none> |
local fixes may depend on goal params;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
4a6d4dcb |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
d3dc194f |
|
20-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
d3c329d2 |
|
16-Oct-2012 |
wenzelm <none@none> |
clarified defer/prefer: more specific errors;
|
#
ca981f61 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
#
ab54c3b1 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
#
10581850 |
|
14-Jan-2012 |
wenzelm <none@none> |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
#
02c8fa88 |
|
05-Nov-2011 |
wenzelm <none@none> |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;
|
#
b811b2f5 |
|
03-Nov-2011 |
wenzelm <none@none> |
tuned signature;
|
#
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
#
cc7b115e |
|
01-Jun-2010 |
berghofe <none@none> |
outer_constraints with original variable names, to ensure that argsP is consistent with args
|
#
08789841 |
|
09-May-2010 |
wenzelm <none@none> |
just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
|
#
41feac86 |
|
09-May-2010 |
wenzelm <none@none> |
added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
|
#
92bdacd4 |
|
21-Mar-2010 |
wenzelm <none@none> |
Logic.mk_of_sort convenience;
|
#
bbc8cf56 |
|
20-Mar-2010 |
wenzelm <none@none> |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
#
2f14c9ed |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated redundant bindings;
|
#
8518a24a |
|
29-Sep-2009 |
wenzelm <none@none> |
modernized Balanced_Tree;
|
#
0dd59c91 |
|
16-Jul-2009 |
wenzelm <none@none> |
tuned incr_tvar_same; export tuned version of incr_indexes_same;
|
#
9f96bed9 |
|
16-Jul-2009 |
wenzelm <none@none> |
export incr_tvar_same; tuned;
|
#
ce2cffe2 |
|
16-Jul-2009 |
wenzelm <none@none> |
use structure Same; tuned;
|
#
a8f46554 |
|
15-Jul-2009 |
wenzelm <none@none> |
removed obsolete/unused legacy_varify;
|
#
3940bb43 |
|
15-Jul-2009 |
wenzelm <none@none> |
tuned comment;
|
#
b9c2cb8d |
|
13-Jul-2009 |
wenzelm <none@none> |
removed obsolete/unused legacy_unvarify;
|
#
d3c4afac |
|
09-Jul-2009 |
wenzelm <none@none> |
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
|
#
2bcff546 |
|
06-Jul-2009 |
wenzelm <none@none> |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
#
33abb9e3 |
|
16-Mar-2009 |
wenzelm <none@none> |
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
|
#
b1ef46dc |
|
08-Mar-2009 |
wenzelm <none@none> |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
#
e3913b9b |
|
04-Mar-2009 |
wenzelm <none@none> |
renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
|
#
7b9e1a05 |
|
31-Dec-2008 |
wenzelm <none@none> |
qualified Term.rename_wrt_term;
|
#
b08c2db5 |
|
19-Nov-2008 |
wenzelm <none@none> |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
#
0b99b772 |
|
01-Oct-2008 |
wenzelm <none@none> |
tuned comments;
|
#
6506010c |
|
23-Jun-2008 |
wenzelm <none@none> |
added all, is_all; improved dest_all; added implies (from term.ML);
|
#
a6067101 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated theory ProtoPure;
|
#
d5272fc3 |
|
21-Jan-2008 |
berghofe <none@none> |
Removed Logic.auto_rename.
|
#
0e30ca26 |
|
04-Oct-2007 |
wenzelm <none@none> |
replaced literal 'a by Name.aT;
|
#
345bff3e |
|
14-Aug-2007 |
wenzelm <none@none> |
moved support for primitive defs to primitive_defs.ML;
|
#
322e8ea9 |
|
05-Jul-2007 |
wenzelm <none@none> |
simplified has_meta_prems;
|
#
b57ed59c |
|
19-Jun-2007 |
wenzelm <none@none> |
balanced conjunctions;
|
#
e5f2672e |
|
12-Jun-2007 |
wenzelm <none@none> |
removed unused is_atomic;
|
#
4eb2f7b7 |
|
04-Jun-2007 |
wenzelm <none@none> |
added is_atomic; removed unused is_all;
|
#
8d01636e |
|
09-May-2007 |
wenzelm <none@none> |
removed unused mk_cond_defpair;
|
#
b7957923 |
|
28-Nov-2006 |
wenzelm <none@none> |
simplified Logic.count_prems;
|
#
e6d811cf |
|
24-Nov-2006 |
wenzelm <none@none> |
added type_map;
|
#
bec7887c |
|
13-Oct-2006 |
berghofe <none@none> |
Repaired strip_assums_hyp (now also works for goals not in hhf normal form).
|
#
3375775e |
|
06-Oct-2006 |
wenzelm <none@none> |
removed is_equals, is_implies; tuned;
|
#
7fabb1a3 |
|
19-Sep-2006 |
wenzelm <none@none> |
added name_classrel/arities/arity;
|
#
e69dd782 |
|
15-Sep-2006 |
wenzelm <none@none> |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
#
cb7b220c |
|
10-Jul-2006 |
wenzelm <none@none> |
replaced Term.variant(list) by Name.variant(_list); Name.invent_list;
|
#
83d9d3cf |
|
13-Jun-2006 |
wenzelm <none@none> |
(un)varify: tuned exceptions;
|
#
24ff5941 |
|
06-Jun-2006 |
wenzelm <none@none> |
renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
|
#
222e0624 |
|
05-Jun-2006 |
wenzelm <none@none> |
support embedded terms;
|
#
b0f61621 |
|
12-Apr-2006 |
wenzelm <none@none> |
added dest_conjunction_list; close_form: canonical order of variables;
|
#
91decbb7 |
|
11-Apr-2006 |
wenzelm <none@none> |
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;
|
#
8855a393 |
|
09-Apr-2006 |
wenzelm <none@none> |
Term.itselfT;
|
#
054b0614 |
|
22-Feb-2006 |
wenzelm <none@none> |
simplified Pure conjunction, based on actual const;
|
#
68d0f14a |
|
18-Feb-2006 |
wenzelm <none@none> |
dest_def: tuned error msg;
|
#
e7f9b0ca |
|
16-Feb-2006 |
wenzelm <none@none> |
dest_def: actually return beta-eta contracted equation;
|
#
a6319250 |
|
07-Feb-2006 |
wenzelm <none@none> |
renamed gen_duplicates to duplicates;
|
#
866d1ba0 |
|
06-Feb-2006 |
wenzelm <none@none> |
added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);
|
#
55bcda07 |
|
23-Jan-2006 |
wenzelm <none@none> |
added dest_all;
|
#
fc63d7b4 |
|
23-Dec-2005 |
wenzelm <none@none> |
added mk_conjunction_list2;
|
#
591392ab |
|
21-Dec-2005 |
wenzelm <none@none> |
mk_conjunction: proper treatment of bounds; added dest_conjunction(s);
|
#
fcab2487 |
|
25-Nov-2005 |
wenzelm <none@none> |
tuned;
|
#
7e820437 |
|
16-Nov-2005 |
wenzelm <none@none> |
tuned;
|
#
1b632ab1 |
|
28-Oct-2005 |
wenzelm <none@none> |
renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;
|
#
bd98e026 |
|
18-Aug-2005 |
paulson <none@none> |
optimization to incr_indexes?
|
#
17b633c2 |
|
19-Jul-2005 |
wenzelm <none@none> |
incr_tvar (from term.ML), incr_indexes: avoid garbage;
|
#
f0fdc3f0 |
|
15-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
6755fbde |
|
14-Jul-2005 |
wenzelm <none@none> |
occs no longer infix (structure not open);
|
#
424b1e92 |
|
31-May-2005 |
wenzelm <none@none> |
added nth_prem;
|
#
f527ae4a |
|
09-Mar-2005 |
ballarin <none@none> |
First version of global registration command.
|
#
f993d1a6 |
|
23-Jan-2005 |
paulson <none@none> |
thin_tac now works on P==>Q
|
#
2547efef |
|
21-Jan-2005 |
paulson <none@none> |
fixed thin_tac with higher-level assumptions by removing the old code to handle the iterated introduction of parameters
|
#
0c10a3d2 |
|
30-Jul-2003 |
berghofe <none@none> |
Removed extraneous rev in function goal_params (the list of parameters is already reversed by rename_wrt_term).
|
#
032bf4f9 |
|
11-Jul-2003 |
berghofe <none@none> |
Exported function goal_params.
|
#
2c2775da |
|
03-Feb-2003 |
berghofe <none@none> |
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
|
#
05da229d |
|
21-Oct-2002 |
berghofe <none@none> |
Removed obsolete functions dealing with flex-flex constraints.
|
#
57ba2cfd |
|
19-Feb-2002 |
wenzelm <none@none> |
Symbol.bump_string;
|
#
d5d19219 |
|
17-Jan-2002 |
wenzelm <none@none> |
is_norm_hhf moved to drule.ML;
|
#
1ed8b62d |
|
14-Jan-2002 |
wenzelm <none@none> |
added mk_conjunction_list;
|
#
e56a0c2a |
|
11-Nov-2001 |
wenzelm <none@none> |
added mk_conjunction;
|
#
ba23e385 |
|
07-Jan-2001 |
wenzelm <none@none> |
added is_norm_hhf;
|
#
da79f4de |
|
10-Nov-2000 |
wenzelm <none@none> |
has_meta_prems: include "==";
|
#
8c9a887d |
|
24-Aug-2000 |
paulson <none@none> |
fixed strip_assums and assum_pairs, restoring them (essentially) to their 1989 versions. They had been "optimized" for flattened parameters, but failed when given an initial, non-flattened proof state. A manifestation of the bug is Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))"; be exE 1;
|
#
de1b43e4 |
|
21-Aug-2000 |
wenzelm <none@none> |
fixed has_meta_prems: strip_assums_hyp;
|
#
daa0542c |
|
31-Jul-2000 |
wenzelm <none@none> |
added has_meta_prems;
|
#
c2a3a791 |
|
29-Jul-2000 |
wenzelm <none@none> |
Logic.goal_const;
|
#
32f99294 |
|
17-Jun-1998 |
nipkow <none@none> |
Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
|
#
6a865eae |
|
22-Apr-1998 |
wenzelm <none@none> |
added mk_cond_defpair, mk_defpair;
|
#
227a394c |
|
09-Mar-1998 |
wenzelm <none@none> |
adapted to baroque chars;
|
#
786ed4df |
|
04-Mar-1998 |
nipkow <none@none> |
Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
|
#
36cc27e4 |
|
28-Feb-1998 |
nipkow <none@none> |
Tried to reorganize rewriter a little. More to be done.
|
#
b3af9d7d |
|
18-Feb-1998 |
nipkow <none@none> |
Improved loop-test for rewrite rules a little. Should be done properly!
|
#
db4d1f8b |
|
19-Dec-1997 |
wenzelm <none@none> |
term order stuff moved to term.ML;
|
#
53d6f089 |
|
01-Dec-1997 |
wenzelm <none@none> |
tuned term order; added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;
|
#
823c8b01 |
|
27-Nov-1997 |
nipkow <none@none> |
Fixed the definition of `termord': is now antisymmetric.
|
#
f19cb486 |
|
03-Nov-1997 |
nipkow <none@none> |
logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.
|
#
b2ad71e7 |
|
21-Oct-1997 |
nipkow <none@none> |
Corrected alphabetical order of entries in signature.
|
#
c4b46290 |
|
17-Oct-1997 |
paulson <none@none> |
Added "op" before "occs" to make sml/nj happy
|
#
6b5139e3 |
|
16-Oct-1997 |
nipkow <none@none> |
The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.
|
#
743eb284 |
|
05-Jun-1997 |
paulson <none@none> |
Removal of freeze_vars and thaw_vars (quite unused...)
|
#
1f73d483 |
|
16-Jan-1997 |
wenzelm <none@none> |
added term order;
|
#
a03b75ec |
|
28-Nov-1996 |
paulson <none@none> |
Replaced map...~~ by ListPair.map
|
#
7260dbc5 |
|
28-Jun-1996 |
paulson <none@none> |
Restored warning comment
|
#
f54858a0 |
|
15-Feb-1996 |
paulson <none@none> |
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
|
#
ecb6e3c2 |
|
29-Jan-1996 |
clasohm <none@none> |
inserted tabs again
|
#
385672e0 |
|
29-Jan-1996 |
clasohm <none@none> |
removed tabs
|
#
ed876d67 |
|
12-Oct-1994 |
wenzelm <none@none> |
added is_equals: term -> bool;
|
#
7a3a551e |
|
06-Sep-1994 |
lcp <none@none> |
Pure/type/unvarifyT: moved there from logic.ML
|
#
6c47a87b |
|
18-Aug-1994 |
lcp <none@none> |
/unvarifyT, unvarify: moved to Pure/logic.ML
|
#
ed17a4e7 |
|
06-Jul-1994 |
wenzelm <none@none> |
changed comment only;
|
#
3fc6c4d8 |
|
26-May-1994 |
wenzelm <none@none> |
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses); restored functor sig constraint :LOGIC;
|
#
1fbf2024 |
|
04-Jan-1994 |
wenzelm <none@none> |
commented out sig constraint of functor (for debugging purposes);
|
#
5d297d4f |
|
21-Oct-1993 |
lcp <none@none> |
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of. So it no longer checks t properly -- but it never checked u anyway, and all existing calls are derived from certified terms...
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|