| #
ea8a815a |
|
13-Jan-2019 |
wenzelm <none@none> |
tuned;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
e2c34057 |
|
21-Jun-2018 |
wenzelm <none@none> |
clarified signature;
|
| #
c70da870 |
|
24-Jun-2017 |
haftmann <none@none> |
treat "undefined" constants internally as special form of case combinators
--HG--
extra : rebase_source : 7a14d2c63e99b8e4fd540a533af3dac408ee1d0e
|
| #
878b6f4b |
|
13-Apr-2017 |
haftmann <none@none> |
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
--HG--
extra : rebase_source : e408c1077f16249a98b1375329604e6e90339e0c
|
| #
9c2a5aeb |
|
26-Jan-2017 |
haftmann <none@none> |
tuned structure and terminology
--HG--
extra : rebase_source : 6302be51f0fe04b147a05d82b816c7a5aa4023ea
|
| #
1a3088a0 |
|
14-Jun-2016 |
haftmann <none@none> |
explicit resolution of ambiguous dictionaries
|
| #
11603865 |
|
29-May-2016 |
haftmann <none@none> |
explicit check that abstract constructors cannot be part of official interface
|
| #
e1b5cf61 |
|
26-May-2016 |
haftmann <none@none> |
optional timing for code generator conversions
|
| #
f1e6947d |
|
26-May-2016 |
haftmann <none@none> |
corrected closure scope of static_conv_thingol;
clarified implementation and names
|
| #
eec6cf97 |
|
26-May-2016 |
haftmann <none@none> |
clarified proof context vs. background theory
|
| #
10135f7d |
|
26-May-2016 |
haftmann <none@none> |
clarified naming conventions and code for code evaluation sandwiches
|
| #
80946636 |
|
26-May-2016 |
haftmann <none@none> |
clarified names of variants
|
| #
e409d817 |
|
09-May-2016 |
wenzelm <none@none> |
clarified context, notably for internal use of Simplifier;
|
| #
8930b173 |
|
08-Mar-2016 |
haftmann <none@none> |
explicit record values for dictionary variables
|
| #
56f8495e |
|
08-Mar-2016 |
haftmann <none@none> |
provide explicit hint concering uniqueness of derivation
|
| #
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
| #
6033868f |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned signature: eliminated pointless type Context.pretty;
|
| #
4e1bdd2c |
|
08-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
| #
3a3f0be1 |
|
16-Apr-2015 |
wenzelm <none@none> |
discontinued pointless warnings: commands are only defined inside a theory context;
|
| #
d60a34e3 |
|
16-Apr-2015 |
wenzelm <none@none> |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
ec0573b0 |
|
24-Mar-2015 |
wenzelm <none@none> |
clarified input source;
|
| #
999d1f7a |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
20eca25a |
|
15-Feb-2015 |
haftmann <none@none> |
tuned
|
| #
7a91cef1 |
|
15-Feb-2015 |
haftmann <none@none> |
purge variables not mentioned in body from pattern
|
| #
1ec2f601 |
|
14-Feb-2015 |
haftmann <none@none> |
only collapse patterns with disjunctive variable names
|
| #
b78864d6 |
|
14-Feb-2015 |
haftmann <none@none> |
clarified
|
| #
8e3951be |
|
31-Dec-2014 |
wenzelm <none@none> |
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
tuned;
|
| #
9e7e597c |
|
31-Dec-2014 |
wenzelm <none@none> |
for graph display, prefer graph data structure over list with dependencies;
pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes
|
| #
e9ab32e2 |
|
31-Dec-2014 |
wenzelm <none@none> |
more explict and generic field names
|
| #
9998c90d |
|
31-Dec-2014 |
wenzelm <none@none> |
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
1f6164d3 |
|
27-Apr-2015 |
wenzelm <none@none> |
code equations as displayable content in code dependency graph
|
| #
3ad9f88a |
|
27-Apr-2015 |
wenzelm <none@none> |
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
clarified
|
| #
7ee8e540 |
|
03-Nov-2014 |
wenzelm <none@none> |
eliminated unused int_only flag (see also c12484a27367);
just proper commands;
|
| #
011d7c60 |
|
18-Sep-2014 |
haftmann <none@none> |
tuned data structure
--HG--
extra : rebase_source : 7cc408d038ae0cb3e103cd433b0b20a81851b688
|
| #
7bb811e1 |
|
15-May-2014 |
haftmann <none@none> |
syntactic means to prevent accidental mixup of static and dynamic context
--HG--
extra : rebase_source : 5713560aaa0dd320d68157ba353db0f597594d25
|
| #
c0fb38de |
|
15-May-2014 |
haftmann <none@none> |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
--HG--
extra : rebase_source : 9e5c02ee3f9e1ecf4b01a5b399ce2acc72f323e2
|
| #
89defae1 |
|
09-May-2014 |
haftmann <none@none> |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
tuned naming;
dropped dead parameters;
|
| #
9e3bb39c |
|
01-May-2014 |
haftmann <none@none> |
optional case enforcement
--HG--
extra : rebase_source : 9cdeaf7fca2e9c8512cef2a7a8af271ea0daed50
|
| #
81d6c2a2 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
3475d7e6 |
|
12-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
98c7fb02 |
|
10-Mar-2014 |
wenzelm <none@none> |
abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
|
| #
0e1799d7 |
|
01-Mar-2014 |
wenzelm <none@none> |
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
|
| #
e41a1507 |
|
26-Feb-2014 |
haftmann <none@none> |
prefer proof context over background theory
--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e
|
| #
5650e65e |
|
30-Jan-2014 |
haftmann <none@none> |
dependency reporting for code generation errors
--HG--
extra : rebase_source : b7d4ec5b462baf9e4afdcc3772abf185c9505185
|
| #
36baadb8 |
|
30-Jan-2014 |
haftmann <none@none> |
more abstract dictionary construction
--HG--
extra : rebase_source : 072ddc88b4cffdfa180942d2da5b1cb812a11c3e
|
| #
a3f9e497 |
|
30-Jan-2014 |
haftmann <none@none> |
reduced prominence of "permissive code generation"
--HG--
extra : rebase_source : 6e3c6c0e5bf55230da69faeeef775ffe97198728
|
| #
07ad0bb4 |
|
25-Jan-2014 |
haftmann <none@none> |
less clumsy namespace
|
| #
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
| #
41393baf |
|
06-Jan-2014 |
haftmann <none@none> |
special treatment of ==> and == solely as constants
|
| #
71765c99 |
|
06-Jan-2014 |
haftmann <none@none> |
uniform orientation of instances as (type constructor, type class)
|
| #
befed50f |
|
31-Dec-2013 |
haftmann <none@none> |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
| #
62f7d300 |
|
30-Jul-2013 |
wenzelm <none@none> |
proper PIDE markup for codegen arguments;
|
| #
3e492425 |
|
04-Jul-2013 |
haftmann <none@none> |
explicit hint for domain of class parameters in instance statements
|
| #
8fa4b40e |
|
26-May-2013 |
wenzelm <none@none> |
tuned;
|
| #
8efa9794 |
|
24-May-2013 |
haftmann <none@none> |
bookkeeping and input syntax for exact specification of names of symbols in generated code
--HG--
extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0
|
| #
0fe14a59 |
|
10-Apr-2013 |
wenzelm <none@none> |
more standard module name Axclass (according to file name);
|
| #
59410e28 |
|
09-Apr-2013 |
wenzelm <none@none> |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;
|
| #
250a6691 |
|
27-Dec-2012 |
haftmann <none@none> |
more explicit name
|
| #
53ab0ad7 |
|
25-Sep-2012 |
wenzelm <none@none> |
separate module Graph_Display;
tuned signature;
|
| #
fe5c2c2b |
|
04-Jun-2012 |
haftmann <none@none> |
clarified code translation code
|
| #
dc977d45 |
|
04-Jun-2012 |
haftmann <none@none> |
prefer records with speaking labels over deeply nested tuples
--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0
|
| #
8ceda7e9 |
|
28-May-2012 |
haftmann <none@none> |
dropped sort constraints on datatype specifications
|
| #
d8b8c922 |
|
19-Apr-2012 |
haftmann <none@none> |
dropped dead code;
tuned
--HG--
extra : rebase_source : 3548e686e93188249306305b2ce26a36c18ce819
|
| #
75375f65 |
|
19-Apr-2012 |
haftmann <none@none> |
tuned
|
| #
86c57deb |
|
18-Apr-2012 |
haftmann <none@none> |
tuned name
--HG--
extra : rebase_source : a9c50c34a64b980c0c55247c493cac4218be224c
|
| #
3faae473 |
|
18-Apr-2012 |
haftmann <none@none> |
tuned
|
| #
3307eb21 |
|
12-Apr-2012 |
Andreas Lochbihler <none@none> |
generalise case certificates to allow ignored parameters
|
| #
551b966c |
|
18-Mar-2012 |
wenzelm <none@none> |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;
|
| #
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
| #
50dbbcde |
|
24-Feb-2012 |
wenzelm <none@none> |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
| #
9f564a6a |
|
23-Feb-2012 |
wenzelm <none@none> |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
| #
b7dd970b |
|
26-Dec-2011 |
haftmann <none@none> |
dropped disfruitful `constant signatures`
|
| #
69ab8127 |
|
19-Oct-2011 |
bulwahn <none@none> |
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
|
| #
a363c5f7 |
|
12-Oct-2011 |
wenzelm <none@none> |
discontinued obsolete alias structure ProofContext;
|
| #
5a712294 |
|
20-Sep-2011 |
bulwahn <none@none> |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
| #
899458fb |
|
19-Sep-2011 |
bulwahn <none@none> |
adding abstraction layer; more precise function names
|
| #
0927ed7e |
|
19-Sep-2011 |
bulwahn <none@none> |
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
|
| #
f76ef76f |
|
19-Sep-2011 |
bulwahn <none@none> |
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
|
| #
4d1e3e48 |
|
19-Sep-2011 |
bulwahn <none@none> |
only annotating constants with sort constraints
|
| #
090d6685 |
|
19-Sep-2011 |
bulwahn <none@none> |
also adding type annotations for the dynamic invocation
|
| #
5423006f |
|
09-Sep-2011 |
bulwahn <none@none> |
stating more explicitly our expectation that these two terms have the same term structure
|
| #
7bd67c7f |
|
08-Sep-2011 |
bulwahn <none@none> |
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
|
| #
6168fc3c |
|
07-Sep-2011 |
bulwahn <none@none> |
removing previously used function locally_monomorphic in the code generator
|
| #
cfca69eb |
|
07-Sep-2011 |
bulwahn <none@none> |
setting const_sorts to false in the type inference of the code generator
|
| #
81f7f7e1 |
|
07-Sep-2011 |
bulwahn <none@none> |
removing previous crude approximation to add type annotations to disambiguate types
|
| #
b41a4b70 |
|
07-Sep-2011 |
bulwahn <none@none> |
adding minimalistic implementation for printing the type annotations
|
| #
729cd46b |
|
07-Sep-2011 |
bulwahn <none@none> |
adding call to disambiguation annotations
|
| #
b1a376b4 |
|
07-Sep-2011 |
bulwahn <none@none> |
adding type inference for disambiguation annotations in code equation
|
| #
20767fdb |
|
07-Sep-2011 |
bulwahn <none@none> |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
| #
0b9a2ceb |
|
07-Sep-2011 |
bulwahn <none@none> |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
| #
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;
|
| #
1a5a42ee |
|
09-Jun-2011 |
wenzelm <none@none> |
simplified Name.variant -- discontinued builtin fold_map;
|
| #
643ddb0f |
|
30-May-2011 |
bulwahn <none@none> |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
| #
3177e5c8 |
|
17-Apr-2011 |
wenzelm <none@none> |
simplified Sorts.class_error: plain Proof.context;
tuned;
|
| #
dbff82ee |
|
18-Apr-2011 |
wenzelm <none@none> |
simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
e56c255d |
|
16-Apr-2011 |
wenzelm <none@none> |
prefer local name spaces;
tuned signatures;
tuned;
|
| #
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
| #
661be15b |
|
17-Feb-2011 |
haftmann <none@none> |
added is_IAbs; tuned brackets and comments
|
| #
b6632ba0 |
|
21-Dec-2010 |
haftmann <none@none> |
proper static closures
|
| #
805df3e0 |
|
21-Dec-2010 |
haftmann <none@none> |
canonical handling of theory context argument
|
| #
20f5e440 |
|
15-Dec-2010 |
haftmann <none@none> |
simplified evaluation function names
|
| #
095d592f |
|
13-Dec-2010 |
haftmann <none@none> |
separated dictionary weakning into separate type
|
| #
e48262e7 |
|
09-Dec-2010 |
haftmann <none@none> |
dictionary constants must permit explicit weakening of classes;
tuned names
|
| #
3c9f234d |
|
01-Dec-2010 |
wenzelm <none@none> |
more direct use of binder_types/body_type;
|
| #
867d43dc |
|
26-Nov-2010 |
haftmann <none@none> |
keep type variable arguments of datatype constructors in bookkeeping
|
| #
1406b8d8 |
|
25-Nov-2010 |
haftmann <none@none> |
globbing constant expressions use more idiomatic underscore rather than star
|
| #
899bcfb0 |
|
20-Sep-2010 |
haftmann <none@none> |
Pure equality is a regular cpde operation
|
| #
634cfb9f |
|
17-Sep-2010 |
haftmann <none@none> |
proper closures for static evaluation; no need for FIXMEs any longer
|
| #
37ee3440 |
|
16-Sep-2010 |
haftmann <none@none> |
separation of static and dynamic thy context
|
| #
0a9e43b6 |
|
15-Sep-2010 |
haftmann <none@none> |
ignore code cache optionally
|
| #
5391ae4f |
|
07-Sep-2010 |
haftmann <none@none> |
dropped outdated substitution
|
| #
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
| #
58d9f816 |
|
23-Aug-2010 |
haftmann <none@none> |
preliminary versions of static_eval_conv(_simple)
|
| #
0f2a759e |
|
23-Aug-2010 |
haftmann <none@none> |
refined and unified naming convention for dynamic code evaluation techniques
|
| #
b595d847 |
|
21-Jul-2010 |
wenzelm <none@none> |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
| #
3140d252 |
|
16-Jul-2010 |
haftmann <none@none> |
don't fail gracefully
|
| #
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
| #
2c3a216a |
|
05-Jul-2010 |
haftmann <none@none> |
dropped passed irregular names
|
| #
34b8f3d1 |
|
02-Jul-2010 |
haftmann <none@none> |
reverted to verion from fc27be4c6b1c
|
| #
2682c3b7 |
|
02-Jul-2010 |
haftmann <none@none> |
traceback for error messages
|
| #
199c29d4 |
|
30-Jun-2010 |
haftmann <none@none> |
unfold_fun_n
|
| #
ec22e3ba |
|
17-Jun-2010 |
haftmann <none@none> |
explicit type variable arguments for constructors
|
| #
3032d8aa |
|
17-Jun-2010 |
haftmann <none@none> |
transitive superclasses were also only a misunderstanding
|
| #
233f64f3 |
|
17-Jun-2010 |
haftmann <none@none> |
formal introduction of transitive superclasses
|
| #
7f4e9daa |
|
17-Jun-2010 |
haftmann <none@none> |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
| #
7cba7845 |
|
15-Jun-2010 |
haftmann <none@none> |
maintain cong rules for case combinators; more precise permissiveness
|
| #
93fbbd8f |
|
15-Jun-2010 |
haftmann <none@none> |
formal introduction of case cong
|
| #
c3a226ee |
|
14-Jun-2010 |
haftmann <none@none> |
teaked naming of superclass projections
|
| #
5c97a57f |
|
07-Jun-2010 |
haftmann <none@none> |
more consistent naming aroud type classes and instances
|
| #
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
| #
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
|
| #
f137a980 |
|
21-Apr-2010 |
haftmann <none@none> |
optionally ignore errors during translation of equations; tuned representation of abstraction points
|
| #
d322f545 |
|
19-Apr-2010 |
haftmann <none@none> |
more appropriate representation of valid positions for abstractors
|
| #
06b4848e |
|
11-Apr-2010 |
wenzelm <none@none> |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
| #
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;
|
| #
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;
|
| #
9bbce8ca |
|
22-Feb-2010 |
haftmann <none@none> |
proper distinction of code datatypes and abstypes
|
| #
e7d798ad |
|
19-Feb-2010 |
haftmann <none@none> |
a simple concept for datatype invariants
|
| #
8aec09fd |
|
12-Jan-2010 |
haftmann <none@none> |
explicit abstract type of code certificates
|
| #
ab05ef6e |
|
12-Jan-2010 |
haftmann <none@none> |
code certificates as integral part of code generation
|
| #
a63742b0 |
|
04-Jan-2010 |
haftmann <none@none> |
code cache only persists on equal theories
|
| #
d464e9a4 |
|
04-Jan-2010 |
haftmann <none@none> |
code cache without copy; tuned
|
| #
b9199a91 |
|
23-Dec-2009 |
haftmann <none@none> |
reduced code generator cache to the baremost minimum
|
| #
299f663d |
|
14-Dec-2009 |
haftmann <none@none> |
explicit name for function space
|
| #
2112c50f |
|
07-Dec-2009 |
haftmann <none@none> |
repaired read_const_expr, broken in 1e7ca47c6c3d
|
| #
36c66eb0 |
|
04-Dec-2009 |
haftmann <none@none> |
avoid misleading name "superarities"
|
| #
79a7b39d |
|
02-Dec-2009 |
haftmann <none@none> |
subst_signatures
|
| #
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
|
| #
02c48bf5 |
|
25-Nov-2009 |
haftmann <none@none> |
normalized uncurry take/drop
--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9
|
| #
e3772a5e |
|
24-Nov-2009 |
haftmann <none@none> |
curried take/drop
--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0
|
| #
71ec8f6f |
|
03-Nov-2009 |
haftmann <none@none> |
pretty name for ==>
|
| #
b26ae843 |
|
26-Oct-2009 |
haftmann <none@none> |
tuned
|
| #
acdfaae2 |
|
25-Oct-2009 |
wenzelm <none@none> |
maintain theory name via name space, not tags;
AxClass.thynames_of_arity: explicit theory name, not tags;
|
| #
b5f3743b |
|
20-Oct-2009 |
wenzelm <none@none> |
uniform use of Integer.min/max;
|
| #
f20cfda9 |
|
14-Oct-2009 |
haftmann <none@none> |
sharpened name
|
| #
944a496c |
|
13-Oct-2009 |
haftmann <none@none> |
more explicit notion of canonized code equations
|
| #
2b0ffcf9 |
|
12-Oct-2009 |
haftmann <none@none> |
added add_tyconames; tuned
|
| #
eefacf4f |
|
11-Oct-2009 |
haftmann <none@none> |
added is_IVar
|
| #
407840d5 |
|
08-Oct-2009 |
haftmann <none@none> |
added group_stmts
|
| #
13c1d7fc |
|
05-Oct-2009 |
haftmann <none@none> |
tuned handling of type variable names further
|
| #
c6dd10bc |
|
05-Oct-2009 |
haftmann <none@none> |
variables in type schemes must be renamed simultaneously with variables in equations
|
| #
a2b19260 |
|
30-Sep-2009 |
wenzelm <none@none> |
Sorts.of_sort_derivation: no pp here;
|
| #
5cf76af4 |
|
08-Sep-2009 |
haftmann <none@none> |
explicit transfer avoids spurious merge problems
|
| #
0ae74e8a |
|
11-Aug-2009 |
haftmann <none@none> |
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
|
| #
3857e383 |
|
09-Aug-2009 |
haftmann <none@none> |
moved all technical processing of code equations to code_thingol.ML
|
| #
1fd83a10 |
|
10-Aug-2009 |
haftmann <none@none> |
attempt to move desymbolization to translation
|
| #
9270bec9 |
|
29-Jul-2009 |
haftmann <none@none> |
abstractions: desymbolize name hint
|
| #
58689e08 |
|
21-Jul-2009 |
haftmann <none@none> |
integrated add_triv_classes into evaluation stack
|
| #
886198b6 |
|
20-Jul-2009 |
wenzelm <none@none> |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
| #
60dd481b |
|
08-Jul-2009 |
haftmann <none@none> |
tuned structure Code internally
|
| #
eb3d3d40 |
|
07-Jul-2009 |
haftmann <none@none> |
tuned interface of structure Code
|
| #
ab72d3b2 |
|
03-Jul-2009 |
haftmann <none@none> |
cleaned up fundamental iml term functions; nested patterns
|
| #
6ecd879c |
|
30-Jun-2009 |
haftmann <none@none> |
improved treatment of case patterns
|
| #
fe02af32 |
|
30-Jun-2009 |
haftmann <none@none> |
an intermediate step towards a refined translation of cases
|
| #
d811f2f3 |
|
30-Jun-2009 |
haftmann <none@none> |
all variable names are optional
|
| #
890b79ce |
|
30-Jun-2009 |
haftmann <none@none> |
variable names in abstractions are optional
|
| #
4f0af429 |
|
30-Jun-2009 |
haftmann <none@none> |
simplified binding concept
|
| #
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
uniformly capitialized names for subdirectories
--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML
|