#
b06d33d9 |
|
06-Aug-2019 |
wenzelm <none@none> |
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
|
#
86be8a71 |
|
05-Aug-2019 |
wenzelm <none@none> |
clarified modules: more direct data implementation;
|
#
aede6033 |
|
02-Aug-2019 |
wenzelm <none@none> |
clarified modules: inference kernel maintains sort algebra within the logic;
|
#
536970b5 |
|
01-Aug-2019 |
wenzelm <none@none> |
more elementary treatment of standard_vars (unconstrainT is already standard);
|
#
e708113a |
|
20-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
1fe8494d |
|
16-Feb-2018 |
wenzelm <none@none> |
removed unused material;
|
#
ce8caca1 |
|
16-Feb-2018 |
wenzelm <none@none> |
trim context of persistent data;
|
#
e409d817 |
|
09-May-2016 |
wenzelm <none@none> |
clarified context, notably for internal use of Simplifier;
|
#
8ec93140 |
|
06-Apr-2016 |
wenzelm <none@none> |
prefer regular context update, to allow continuous editing of Pure;
|
#
6033868f |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned signature: eliminated pointless type Context.pretty;
|
#
a0dc69c0 |
|
22-Sep-2015 |
wenzelm <none@none> |
tuned signature;
|
#
8ed115e9 |
|
22-Sep-2015 |
wenzelm <none@none> |
eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
|
#
e6c3e275 |
|
22-Sep-2015 |
wenzelm <none@none> |
tuned whitespace;
|
#
13bb5ba7 |
|
22-Sep-2015 |
wenzelm <none@none> |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
7ef34291 |
|
23-Feb-2015 |
wenzelm <none@none> |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
b32c43f2 |
|
12-May-2014 |
wenzelm <none@none> |
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
|
#
8ae5e91a |
|
14-Mar-2014 |
wenzelm <none@none> |
conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';
|
#
3fd6cc4a |
|
10-Feb-2014 |
wenzelm <none@none> |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
#
71765c99 |
|
06-Jan-2014 |
haftmann <none@none> |
uniform orientation of instances as (type constructor, type class)
|
#
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
|
#
a66c9494 |
|
23-Aug-2013 |
wenzelm <none@none> |
added Theory.setup convenience;
|
#
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
#
e0ba4a0b |
|
29-May-2013 |
wenzelm <none@none> |
standardized aliases;
|
#
0fe14a59 |
|
10-Apr-2013 |
wenzelm <none@none> |
more standard module name Axclass (according to file name);
|
#
9e4021ad |
|
10-Apr-2013 |
wenzelm <none@none> |
formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;
|
#
5bb0e68d |
|
07-Jan-2013 |
wenzelm <none@none> |
tuned;
|
#
10b17ef9 |
|
07-Jan-2013 |
wenzelm <none@none> |
tuned -- prefer high-level Table.merge with its slightly more conservative update;
|
#
afcc6e95 |
|
07-Jan-2013 |
wenzelm <none@none> |
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed; transfer theorems where they are picked from the theory; tuned;
|
#
dae9bdf9 |
|
07-Jan-2013 |
wenzelm <none@none> |
tuned comment -- do not claim anything;
|
#
d049bd7b |
|
20-Aug-2011 |
wenzelm <none@none> |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
#
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
#
f9c0ed13 |
|
18-Apr-2011 |
wenzelm <none@none> |
pass plain Proof.context for pretty printing;
|
#
dbff82ee |
|
18-Apr-2011 |
wenzelm <none@none> |
simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
|
#
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
3272990d |
|
17-Dec-2010 |
wenzelm <none@none> |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning; --HG-- rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML
|
#
308c65f5 |
|
20-Sep-2010 |
wenzelm <none@none> |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; --HG-- rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML
|
#
d19dab54 |
|
05-Sep-2010 |
wenzelm <none@none> |
turned show_sorts/show_types into proper configuration options;
|
#
d5fed4bd |
|
05-Sep-2010 |
wenzelm <none@none> |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
#
2cf7654a |
|
11-Aug-2010 |
haftmann <none@none> |
tuned whitespace
|
#
303079d4 |
|
01-Jun-2010 |
haftmann <none@none> |
avoid store flag in add_* operations
|
#
a9a10ad6 |
|
01-Jun-2010 |
haftmann <none@none> |
do not expose store flag of AxClass.add_*
|
#
2bfbdf77 |
|
01-Jun-2010 |
berghofe <none@none> |
classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.
|
#
5f3f7eef |
|
15-May-2010 |
wenzelm <none@none> |
eliminated redundant runtime checks;
|
#
1291e6c1 |
|
14-May-2010 |
krauss <none@none> |
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
|
#
c01ac0b1 |
|
13-May-2010 |
wenzelm <none@none> |
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
|
#
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;
|
#
657d0cdf |
|
08-May-2010 |
wenzelm <none@none> |
back-patching of axclass proofs;
|
#
60d6d298 |
|
03-May-2010 |
wenzelm <none@none> |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
#
463926d7 |
|
28-Apr-2010 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
8fc5e539 |
|
27-Apr-2010 |
wenzelm <none@none> |
removed obsolete sanity check -- Sign.certify_sort is stable;
|
#
fe3b0765 |
|
27-Apr-2010 |
wenzelm <none@none> |
tuned signature;
|
#
608d4985 |
|
27-Apr-2010 |
wenzelm <none@none> |
tuned classrel completion -- bypass composition with reflexive edges;
|
#
da08a6b8 |
|
27-Apr-2010 |
wenzelm <none@none> |
tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
|
#
def078fd |
|
27-Apr-2010 |
wenzelm <none@none> |
tuned aritiy completion -- slightly less intermediate data structures;
|
#
0a499ae3 |
|
27-Apr-2010 |
wenzelm <none@none> |
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
|
#
5a8eeaef |
|
27-Apr-2010 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
97026d87 |
|
26-Apr-2010 |
wenzelm <none@none> |
removed unused AxClass.class_intros;
|
#
0c16feb6 |
|
25-Apr-2010 |
wenzelm <none@none> |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
|
#
8ac64f3d |
|
25-Apr-2010 |
wenzelm <none@none> |
more systematic treatment of data -- avoid slightly odd nested tuples here; tuned;
|
#
f9144b32 |
|
25-Apr-2010 |
wenzelm <none@none> |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
#
2acf688c |
|
25-Apr-2010 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
c9fc11f6 |
|
25-Apr-2010 |
wenzelm <none@none> |
simplified some private bindings;
|
#
3cd9d75c |
|
25-Apr-2010 |
wenzelm <none@none> |
classrel and arity completion by krauss/schropp;
|
#
f3757455 |
|
11-Apr-2010 |
wenzelm <none@none> |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
#
26716d38 |
|
25-Mar-2010 |
wenzelm <none@none> |
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;
|
#
1fc63de7 |
|
25-Mar-2010 |
wenzelm <none@none> |
removed unused AxClass.of_sort derivation;
|
#
b369d0f0 |
|
22-Mar-2010 |
wenzelm <none@none> |
inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
|
#
e2073456 |
|
21-Mar-2010 |
wenzelm <none@none> |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
#
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;
|
#
f36452c7 |
|
09-Mar-2010 |
wenzelm <none@none> |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
|
#
227c8de0 |
|
19-Feb-2010 |
wenzelm <none@none> |
Thm.def_binding;
|
#
cf637b97 |
|
18-Feb-2010 |
wenzelm <none@none> |
axclass: more precise treatment of naming vs. binding;
|
#
2396d686 |
|
07-Feb-2010 |
wenzelm <none@none> |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
#
ba7958fc |
|
04-Jan-2010 |
wenzelm <none@none> |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
#
babb7ef8 |
|
04-Jan-2010 |
haftmann <none@none> |
dropped copy operation for legacy TheoryDataFun
|
#
71c651db |
|
29-Nov-2009 |
haftmann <none@none> |
dropped some unused bindings --HG-- rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML extra : rebase_source : f9974e246b201df041a994a3a755319b83bce2a3
|
#
32b046a5 |
|
29-Oct-2009 |
wenzelm <none@none> |
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
|
#
ca381023 |
|
28-Oct-2009 |
wenzelm <none@none> |
conceal internal bindings;
|
#
98fa2344 |
|
25-Oct-2009 |
wenzelm <none@none> |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
#
acdfaae2 |
|
25-Oct-2009 |
wenzelm <none@none> |
maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
|
#
cedbaf88 |
|
22-Oct-2009 |
haftmann <none@none> |
explicit close_derivation
|
#
b2816004 |
|
17-Oct-2009 |
wenzelm <none@none> |
indicate CRITICAL nature of various setmp combinators;
|
#
0001a658 |
|
30-Sep-2009 |
wenzelm <none@none> |
removed dead code; Sorts.of_sort_derivation: removed unused pp;
|
#
8518a24a |
|
29-Sep-2009 |
wenzelm <none@none> |
modernized Balanced_Tree;
|
#
02665964 |
|
26-Jul-2009 |
wenzelm <none@none> |
Goal.finish: explicit context for printing;
|
#
88bc1546 |
|
06-Jul-2009 |
wenzelm <none@none> |
add_classrel/arity: strip_shyps of stored result;
|
#
5e95080e |
|
06-Jul-2009 |
wenzelm <none@none> |
clarified Thm.of_class/of_sort/class_triv;
|
#
2bcff546 |
|
06-Jul-2009 |
wenzelm <none@none> |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
#
836440db |
|
02-Jul-2009 |
wenzelm <none@none> |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
#
6f4915c7 |
|
24-May-2009 |
haftmann <none@none> |
tuned class user space type system code
|
#
cd0870d2 |
|
19-May-2009 |
haftmann <none@none> |
avoid potential problem with stale theory
|
#
c442ba6f |
|
17-Apr-2009 |
haftmann <none@none> |
formal declaration of undefined parameters after class instantiation
|
#
105fa1e7 |
|
13-Mar-2009 |
haftmann <none@none> |
coherent binding policy with primitive target operations
|
#
3b56b3af |
|
12-Mar-2009 |
wenzelm <none@none> |
renamed sticky_prefix to mandatory_path;
|
#
0b263664 |
|
11-Mar-2009 |
wenzelm <none@none> |
replaced old-style add_path/no_base_names by sticky_prefix;
|
#
b1ef46dc |
|
08-Mar-2009 |
wenzelm <none@none> |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
#
d206ad0e |
|
07-Mar-2009 |
wenzelm <none@none> |
more uniform handling of binding in targets and derived elements;
|
#
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;
|
#
b079e6db |
|
04-Mar-2009 |
haftmann <none@none> |
explicit error message for `improper` instances lacking explicit instance parameter constants
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
0c02a0cf |
|
03-Mar-2009 |
wenzelm <none@none> |
Thm.binding;
|
#
5061c2dd |
|
21-Jan-2009 |
haftmann <none@none> |
binding replaces bstring
|
#
5af31b4e |
|
17-Jan-2009 |
haftmann <none@none> |
close derivation of classrels
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
d0e328c6 |
|
03-Sep-2008 |
wenzelm <none@none> |
Sign.declare_const: Name.binding;
|
#
f31abf48 |
|
02-Sep-2008 |
wenzelm <none@none> |
explicit type Name.binding for higher-specification elements;
|
#
8970202f |
|
27-Aug-2008 |
haftmann <none@none> |
completing arities after subclass instance
|
#
2fac30b5 |
|
14-Aug-2008 |
wenzelm <none@none> |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
#
4da32258 |
|
29-Jul-2008 |
haftmann <none@none> |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
#
31c76652 |
|
24-Jul-2008 |
haftmann <none@none> |
dropped PureThy.note; added PureThy.add_thm
|
#
01994724 |
|
11-Jul-2008 |
wenzelm <none@none> |
Sorts.weaken: abstract argument;
|
#
4906e3bc |
|
11-Jul-2008 |
haftmann <none@none> |
explicit completions of arities
|
#
fad76ad6 |
|
08-Jul-2008 |
haftmann <none@none> |
refined arity property concept
|
#
f7c70f23 |
|
30-Jun-2008 |
haftmann <none@none> |
tagged arities
|
#
70a4fc69 |
|
18-May-2008 |
wenzelm <none@none> |
moved global pretty/string_of functions from Sign to Syntax;
|
#
ff2c7ded |
|
02-Apr-2008 |
haftmann <none@none> |
removed obscure "attach" feature
|
#
fca57105 |
|
10-Mar-2008 |
haftmann <none@none> |
exported suffix
|
#
6c96e639 |
|
08-Jan-2008 |
haftmann <none@none> |
better error reporting
|
#
9192618c |
|
12-Dec-2007 |
haftmann <none@none> |
exported axiomsN
|
#
83cb70a8 |
|
11-Dec-2007 |
haftmann <none@none> |
error handling for pathological cases
|
#
a454a9fe |
|
10-Dec-2007 |
haftmann <none@none> |
moved instance parameter management from class.ML to axclass.ML
|
#
1ecbe3dd |
|
28-Nov-2007 |
haftmann <none@none> |
naming policy for instances
|
#
9e4a967a |
|
11-Oct-2007 |
wenzelm <none@none> |
moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning;
|
#
1797a506 |
|
09-Oct-2007 |
wenzelm <none@none> |
renamed AxClass.get_definition to AxClass.get_info (again); AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
#
d06d005b |
|
08-Oct-2007 |
wenzelm <none@none> |
generic Syntax.pretty/string_of operations;
|
#
c3f145c0 |
|
04-Oct-2007 |
wenzelm <none@none> |
replaced AxClass.param_tyvarname by Name.aT;
|
#
8d942da7 |
|
30-Sep-2007 |
wenzelm <none@none> |
Sign.add_consts_authentic: tags (Markup.property list);
|
#
8279540b |
|
29-Sep-2007 |
wenzelm <none@none> |
Sign.add_const_constraint;
|
#
22c2d663 |
|
26-Sep-2007 |
wenzelm <none@none> |
Sign.minimize/complete_sort;
|
#
9344c4a9 |
|
25-Sep-2007 |
wenzelm <none@none> |
proper Sign operations instead of Theory aliases;
|
#
946ffe1c |
|
23-Sep-2007 |
wenzelm <none@none> |
tuned;
|
#
aa18dd0a |
|
15-Sep-2007 |
haftmann <none@none> |
clarified class interfaces and internals
|
#
6bd7222d |
|
14-Aug-2007 |
wenzelm <none@none> |
avoid low-level tsig;
|
#
a9487610 |
|
19-Jun-2007 |
wenzelm <none@none> |
balanced conjunctions; added split_defined (from conjunction.ML);
|
#
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
#
929fd668 |
|
20-Apr-2007 |
haftmann <none@none> |
moved axclass module closer to core system
|
#
7b89714a |
|
15-Apr-2007 |
wenzelm <none@none> |
Thm.fold_terms;
|
#
bae9892c |
|
03-Apr-2007 |
wenzelm <none@none> |
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
|
#
e16cad86 |
|
02-Mar-2007 |
haftmann <none@none> |
syntax for "class attach const"
|
#
7e57856a |
|
29-Dec-2006 |
haftmann <none@none> |
cleanup
|
#
41361240 |
|
29-Dec-2006 |
wenzelm <none@none> |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
#
0934c366 |
|
28-Dec-2006 |
haftmann <none@none> |
dropped some bookkeeping
|
#
6671f353 |
|
28-Dec-2006 |
wenzelm <none@none> |
tuned msg;
|
#
0b8fbe1e |
|
27-Dec-2006 |
haftmann <none@none> |
fixed misleading error message
|
#
d22b1456 |
|
21-Dec-2006 |
haftmann <none@none> |
code clarifications
|
#
9989d06d |
|
06-Dec-2006 |
wenzelm <none@none> |
reorganized structure Goal vs. Tactic;
|
#
9bd89ef3 |
|
22-Nov-2006 |
haftmann <none@none> |
completed class parameter handling in axclass.ML
|
#
7db39969 |
|
19-Sep-2006 |
wenzelm <none@none> |
Logic.name_classrel/arities;
|
#
e69dd782 |
|
15-Sep-2006 |
wenzelm <none@none> |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
#
3f949d55 |
|
30-Jul-2006 |
wenzelm <none@none> |
Thm.adjust_maxidx;
|
#
de676c26 |
|
12-Jul-2006 |
haftmann <none@none> |
class_of_param instead of class_of
|
#
d18fb037 |
|
07-Jul-2006 |
wenzelm <none@none> |
Goal.prove: context;
|
#
6654a998 |
|
28-Jun-2006 |
haftmann <none@none> |
added lookup function for parameters
|
#
5361b6f6 |
|
23-May-2006 |
wenzelm <none@none> |
axiomatize class: Theory.add_deps;
|
#
ba240566 |
|
20-May-2006 |
wenzelm <none@none> |
class axiomatization: finals;
|
#
0d32b6ff |
|
16-May-2006 |
wenzelm <none@none> |
more abstract interface to classes/arities;
|
#
a61ca0d4 |
|
06-May-2006 |
wenzelm <none@none> |
removed 'concl is' patterns;
|
#
6e8ab914 |
|
05-May-2006 |
wenzelm <none@none> |
of_sort: explicit cache value; simplified internal representation of instances;
|
#
f07448db |
|
01-May-2006 |
wenzelm <none@none> |
tuned;
|
#
3dc219cd |
|
01-May-2006 |
wenzelm <none@none> |
of_sort: option; of_sort: simplified implementation, use Sorts.of_sort_derivation; tuned;
|
#
aef653b9 |
|
01-May-2006 |
wenzelm <none@none> |
of_sort: simplified derivation;
|
#
d767a0e3 |
|
30-Apr-2006 |
wenzelm <none@none> |
renamed add_axclass(_i) to define_axclass(_i); renamed get_info to get_definition; added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities); tuned;
|
#
6afcc68d |
|
29-Apr-2006 |
wenzelm <none@none> |
instances data: mutable cache; added of_sort: interface for derived instances;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
16ce68af |
|
25-Apr-2006 |
wenzelm <none@none> |
get_info: removed 'super' field; added params_of, all_params_of; removed params_of_sort; tuned;
|
#
9b14d1ca |
|
12-Apr-2006 |
wenzelm <none@none> |
reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms;
|
#
71fae80a |
|
11-Apr-2006 |
wenzelm <none@none> |
moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;
|
#
d2d0774d |
|
10-Apr-2006 |
haftmann <none@none> |
fixed value restriction
|
#
20577f27 |
|
09-Apr-2006 |
wenzelm <none@none> |
add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;
|
#
db370929 |
|
11-Mar-2006 |
wenzelm <none@none> |
moved read_class, read/cert_classrel/arity to sign.ML; axclass: moved outer syntax to isar_syn.ML; instance: moved to Tools/class_package.ML; simplified interfaces; tuned;
|
#
d37252ae |
|
24-Feb-2006 |
berghofe <none@none> |
Reverted to old interface of AxClass.add_inst_arity(_i)
|
#
977eca2e |
|
22-Feb-2006 |
wenzelm <none@none> |
renamed class_axms to class_intros;
|
#
81bc7000 |
|
20-Feb-2006 |
haftmann <none@none> |
moved intro_classes from AxClass to ClassPackage
|
#
a6319250 |
|
07-Feb-2006 |
wenzelm <none@none> |
renamed gen_duplicates to duplicates;
|
#
537997b4 |
|
06-Feb-2006 |
wenzelm <none@none> |
Logic.const_of_class/class_of_const;
|
#
a99d82ca |
|
30-Jan-2006 |
haftmann <none@none> |
moved instance Isar command to class_package.ML
|
#
510de6e4 |
|
27-Jan-2006 |
wenzelm <none@none> |
moved theorem tags from Drule to PureThy;
|
#
1d055c4c |
|
23-Jan-2006 |
haftmann <none@none> |
exported after_qed for axclass instance
|
#
acdc5889 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute;
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
e3517f6b |
|
14-Jan-2006 |
wenzelm <none@none> |
sane ERROR handling;
|
#
56e7d651 |
|
04-Jan-2006 |
haftmann <none@none> |
exported read|cert_arity interfaces
|
#
67baf920 |
|
21-Dec-2005 |
wenzelm <none@none> |
Tactic.precise_conjunction_tac;
|
#
d3b022c7 |
|
16-Dec-2005 |
haftmann <none@none> |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
#
d3e3a029 |
|
09-Dec-2005 |
haftmann <none@none> |
oriented result pairs in PureThy
|
#
87c3b641 |
|
08-Nov-2005 |
wenzelm <none@none> |
simplified after_qed;
|
#
8cceae71 |
|
21-Oct-2005 |
wenzelm <none@none> |
Goal.prove;
|
#
004afb66 |
|
19-Oct-2005 |
wenzelm <none@none> |
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
|
#
10169ee5 |
|
14-Oct-2005 |
wenzelm <none@none> |
goal statements: accomodate before_qed argument;
|
#
db589537 |
|
04-Oct-2005 |
wenzelm <none@none> |
minor tweaks for Poplog/ML;
|
#
a943bc7d |
|
28-Sep-2005 |
wenzelm <none@none> |
Theory.add_finals_i;
|
#
347ce55a |
|
20-Sep-2005 |
haftmann <none@none> |
slight adaptions to library changes
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
5dda77ad |
|
13-Sep-2005 |
wenzelm <none@none> |
tuned Isar interfaces; tuned IsarThy.theorem_i;
|
#
2af4cfbf |
|
06-Sep-2005 |
wenzelm <none@none> |
name space prefix is now "c_class" instead of just "c"; export get_info; tuned;
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
3977c870 |
|
16-Aug-2005 |
wenzelm <none@none> |
OuterKeyword;
|
#
0f0b4228 |
|
09-Aug-2005 |
haftmann <none@none> |
exported after_qed for arity proofs
|
#
8f1bf77f |
|
08-Aug-2005 |
ballarin <none@none> |
After_qed takes result argument.
|
#
ad97b898 |
|
20-Jun-2005 |
wenzelm <none@none> |
get_thm(s): Name;
|
#
c01306d6 |
|
17-Jun-2005 |
wenzelm <none@none> |
accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
|
#
9462a0bb |
|
11-Jun-2005 |
wenzelm <none@none> |
refer to name spaces values instead of names;
|
#
bbb70177 |
|
08-Jun-2005 |
wenzelm <none@none> |
got rid of bclass, xclass;
|
#
031200c2 |
|
02-Jun-2005 |
wenzelm <none@none> |
Theory.restore_naming;
|
#
a8bed6a5 |
|
31-May-2005 |
wenzelm <none@none> |
renamed cond_extern to extern;
|
#
9ac56383 |
|
17-May-2005 |
wenzelm <none@none> |
tuned;
|
#
3647f12c |
|
28-Apr-2005 |
wenzelm <none@none> |
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances); keep legacy stuff separate; tuned;
|
#
9bb356e3 |
|
26-Apr-2005 |
wenzelm <none@none> |
export intro_classes_tac;
|
#
9f1ea5d9 |
|
21-Apr-2005 |
wenzelm <none@none> |
superceded by Pure.thy and CPure.thy;
|
#
fc400fb4 |
|
13-Apr-2005 |
wenzelm <none@none> |
*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
|
#
0f8c0167 |
|
13-Apr-2005 |
wenzelm <none@none> |
*** empty log message ***
|
#
50933e3d |
|
10-Apr-2005 |
ballarin <none@none> |
First release of interpretation commands.
|
#
f527ae4a |
|
09-Mar-2005 |
ballarin <none@none> |
First version of global registration command.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
232c4583 |
|
24-Jan-2005 |
berghofe <none@none> |
Adapted to modified interface of PureThy.get_thm(s).
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
4ca8e7a3 |
|
31-May-2004 |
wenzelm <none@none> |
removed obsolete sort 'logic';
|
#
25d68965 |
|
29-May-2004 |
wenzelm <none@none> |
improved output;
|
#
b18c88fa |
|
21-May-2004 |
wenzelm <none@none> |
test_classrel/arity improve error reporting; tuned;
|
#
afbdc738 |
|
01-May-2004 |
wenzelm <none@none> |
improved Term.invent_names;
|
#
5f1627a6 |
|
16-Apr-2004 |
wenzelm <none@none> |
'instance' and intro_classes now handle general sorts;
|
#
d6f4ddf1 |
|
12-Feb-2002 |
wenzelm <none@none> |
got rid of explicit marginal comments (now stripped earlier from input);
|
#
59291a6a |
|
09-Jan-2002 |
wenzelm <none@none> |
simplified IsarThy.theorem_i;
|
#
b9f0880f |
|
14-Dec-2001 |
wenzelm <none@none> |
Term.invent_type_names;
|
#
65b16e12 |
|
04-Dec-2001 |
wenzelm <none@none> |
tuned;
|
#
cadfdab8 |
|
27-Nov-2001 |
wenzelm <none@none> |
theory data: removed obsolete finish method;
|
#
37c2ce11 |
|
08-Nov-2001 |
wenzelm <none@none> |
theory data: finish method;
|
#
631ae667 |
|
04-Nov-2001 |
wenzelm <none@none> |
IsarThy.theorem_i (None, []);
|
#
c4718bb1 |
|
31-Oct-2001 |
wenzelm <none@none> |
IsarThy.theorem_i: no locale;
|
#
91df789e |
|
27-Oct-2001 |
wenzelm <none@none> |
removed obsolete goal_subclass, goal_arity;
|
#
36adfb1c |
|
18-Oct-2001 |
wenzelm <none@none> |
sane internal interfaces for instance;
|
#
658662df |
|
13-Oct-2001 |
wenzelm <none@none> |
IsarThy.theorem_i Drule.internalK;
|
#
ac04eaf9 |
|
31-Aug-2001 |
wenzelm <none@none> |
proper use of invent_names;
|
#
6267d24e |
|
31-Aug-2001 |
wenzelm <none@none> |
tuned headers;
|
#
d0ff3b21 |
|
31-May-2001 |
wenzelm <none@none> |
invent_names
|
#
f9115060 |
|
12-Feb-2001 |
wenzelm <none@none> |
support \<subseteq> syntax in classes/classrel/axclass/instance;
|
#
0c526a35 |
|
21-Nov-2000 |
wenzelm <none@none> |
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
|
#
857b4755 |
|
18-Nov-2000 |
wenzelm <none@none> |
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
|
#
20eca08c |
|
13-Nov-2000 |
wenzelm <none@none> |
tuned IsarThy.theorem_i;
|
#
fefe5619 |
|
23-Oct-2000 |
wenzelm <none@none> |
intro_classes by default;
|
#
f31e97a5 |
|
17-Sep-2000 |
wenzelm <none@none> |
Display.pretty_thm_sg;
|
#
b3590d55 |
|
22-May-2000 |
paulson <none@none> |
eta-expanded to handle value polymorphism
|
#
a7e2725a |
|
21-May-2000 |
wenzelm <none@none> |
adapted to inner syntax of sorts;
|
#
148d4e48 |
|
17-Apr-2000 |
wenzelm <none@none> |
Pretty.chunks;
|
#
9de907a6 |
|
14-Apr-2000 |
wenzelm <none@none> |
intrn_arity: reject type abbreviations;
|
#
3273541c |
|
05-Apr-2000 |
wenzelm <none@none> |
HEADGOAL;
|
#
4b47f47c |
|
18-Mar-2000 |
wenzelm <none@none> |
intro_classes_tac: REPEAT_ALL_NEW;
|
#
80ed161a |
|
12-Mar-2000 |
wenzelm <none@none> |
adapted to new PureThy.add_thms etc.;
|
#
6dae197f |
|
25-Aug-1999 |
wenzelm <none@none> |
expand_classes renamed to intro_classes;
|
#
98acd81a |
|
08-Jul-1999 |
wenzelm <none@none> |
propp: 'concl' patterns;
|
#
28400f30 |
|
25-May-1999 |
wenzelm <none@none> |
formal comments (still dummy);
|
#
0bac8821 |
|
24-May-1999 |
wenzelm <none@none> |
outer syntax keyword classification; no open OuterParse;
|
#
0df59d08 |
|
21-May-1999 |
wenzelm <none@none> |
improved errors;
|
#
0131d134 |
|
30-Apr-1999 |
wenzelm <none@none> |
theory data: copy;
|
#
77c35c2e |
|
17-Mar-1999 |
wenzelm <none@none> |
qualify Theory.sign_of etc.;
|
#
8ce35fca |
|
17-Mar-1999 |
wenzelm <none@none> |
theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;
|
#
cb1aade0 |
|
11-Jan-1999 |
wenzelm <none@none> |
eliminated Attribute structure;
|
#
a2721406 |
|
20-Oct-1998 |
wenzelm <none@none> |
quiet_mode, message;
|
#
8c9a0b82 |
|
15-May-1998 |
wenzelm <none@none> |
witnesses: lookup stored thms instead of axioms;
|
#
8eae77ba |
|
12-May-1998 |
wenzelm <none@none> |
tuned msg;
|
#
cec5b482 |
|
29-Apr-1998 |
wenzelm <none@none> |
adapted to new PureThy.add_axioms_i;
|
#
fe05d47e |
|
28-Oct-1997 |
wenzelm <none@none> |
add_store_axioms_i;
|
#
38412dfa |
|
24-Oct-1997 |
wenzelm <none@none> |
removed add_thms_as_axms;
|
#
ae8c5cea |
|
20-Oct-1997 |
wenzelm <none@none> |
tuned types;
|
#
d01bdaa9 |
|
20-Oct-1997 |
wenzelm <none@none> |
fixed goal_XXX;
|
#
ea80ea14 |
|
20-Oct-1997 |
wenzelm <none@none> |
fixed types of add_XXX; tuned;
|
#
b987f7e7 |
|
13-Oct-1997 |
wenzelm <none@none> |
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
|
#
84c4a1f3 |
|
09-Oct-1997 |
wenzelm <none@none> |
fixed axiom names;
|
#
66930990 |
|
06-Oct-1997 |
wenzelm <none@none> |
eliminated raise_term, raise_typ; new internal forms: add_inst_subclass_i, add_inst_arity_i;
|
#
ab87285c |
|
01-Oct-1997 |
wenzelm <none@none> |
fully qualified names: Theory.add_XXX;
|
#
57f4bc71 |
|
06-Aug-1997 |
wenzelm <none@none> |
added "Proving ..." msgs;
|
#
dc3d9bad |
|
03-Jun-1997 |
wenzelm <none@none> |
eliminated freeze_vars;
|
#
9c5b6878 |
|
16-Apr-1997 |
wenzelm <none@none> |
Sorts.str_of_arity;
|
#
d42856da |
|
21-Feb-1997 |
paulson <none@none> |
Replaced "flat" by the Basis Library function List.concat
|
#
a03b75ec |
|
28-Nov-1996 |
paulson <none@none> |
Replaced map...~~ by ListPair.map
|
#
27ce7eaf |
|
16-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.
|
#
6f6e7577 |
|
01-Sep-1995 |
wenzelm <none@none> |
adapted to new version of shyps-stuff;
|
#
6feb44b0 |
|
01-Aug-1995 |
wenzelm <none@none> |
modified prep_thm_axm to handle shyps; fixed class_axms: class_trivs *first*; improved axclass_tac: now also handles object rules as witnesses;
|
#
55928922 |
|
27-Jul-1995 |
wenzelm <none@none> |
minor fix: instance now raises error if witness axioms don't exist;
|
#
c9983952 |
|
27-Jan-1995 |
wenzelm <none@none> |
instance: now automatically includes defs of current thy node as witnesses;
|
#
af8f257f |
|
12-Oct-1994 |
wenzelm <none@none> |
prove_subclass, prove_arity now exported; minor internal changes;
|
#
a7a81d61 |
|
19-Aug-1994 |
wenzelm <none@none> |
cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;
|
#
079e56d8 |
|
27-Jul-1994 |
wenzelm <none@none> |
added experimental add_defns (actually should be moved somewhere else); minor internal changes;
|
#
a7cd4470 |
|
14-Jul-1994 |
wenzelm <none@none> |
added functor signature constraint;
|
#
54524ca8 |
|
05-Jul-1994 |
wenzelm <none@none> |
various minor changes (names and comments);
|
#
1bbcf581 |
|
15-Jun-1994 |
wenzelm <none@none> |
(beta release)
|
#
cd9af6f5 |
|
26-May-1994 |
wenzelm <none@none> |
axiomatic type class 'package' for Pure (alpha version);
|