2010-04-30 wenzelm 2010-04-30 conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-29 krauss 2010-04-29 hgweb style: show author in filelog; full description in annotate hover
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29 wenzelm 2010-04-29 read_const: disallow internal names as usual in visible Isar text;
2010-04-29 wenzelm 2010-04-29 more explicit treatment of context, although not fully localized;
2010-04-29 wenzelm 2010-04-29 removed some Emacs junk;
2010-04-29 haftmann 2010-04-29 merged
2010-04-29 haftmann 2010-04-29 make random engine persistent using code_reflect
2010-04-29 haftmann 2010-04-29 repaired subtle misunderstanding: statement names are only passed for name resolution
2010-04-29 haftmann 2010-04-29 fixed underscore typo
2010-04-29 haftmann 2010-04-29 more coherent naming with ML serializer
2010-04-29 haftmann 2010-04-29 dropped code_datatype antiquotation
2010-04-29 haftmann 2010-04-29 dropped unnecessary ML code
2010-04-29 haftmann 2010-04-29 avoid popular infixes
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-29 haftmann 2010-04-29 NEWS: code_reflect
2010-04-29 haftmann 2010-04-29 merged
2010-04-28 haftmann 2010-04-28 updated generated file
2010-04-28 haftmann 2010-04-28 modernized structure name
2010-04-28 haftmann 2010-04-28 use code_reflect
2010-04-29 wenzelm 2010-04-29 merged
2010-04-29 Cezary Kaliszyk 2010-04-29 Tuning the quotient examples
2010-04-28 krauss 2010-04-28 clarified signature; simpler implementation in terms of function's tactic interface
2010-04-28 krauss 2010-04-28 return info record (relative to auxiliary context!)
2010-04-28 krauss 2010-04-28 default termination prover as plain tactic
2010-04-28 krauss 2010-04-28 function: sane interface for programmatic use
2010-04-28 krauss 2010-04-28 ML interface uses plain command names, following conventions from typedef
2010-04-28 krauss 2010-04-28 function: better separate Isar integration from actual functionality
2010-04-29 haftmann 2010-04-29 merged
2010-04-28 haftmann 2010-04-28 export somehow odd mapa explicitly
2010-04-28 haftmann 2010-04-28 exported print_tuple
2010-04-28 haftmann 2010-04-28 take into account tupled constructors
2010-04-28 haftmann 2010-04-28 avoid code_datatype antiquotation
2010-04-28 bulwahn 2010-04-28 merged
2010-04-28 bulwahn 2010-04-28 added an example with a free function variable to the Predicate Compile examples
2010-04-28 bulwahn 2010-04-28 removed local clone in the predicate compiler
2010-04-28 bulwahn 2010-04-28 improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
2010-04-29 wenzelm 2010-04-29 allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
2010-04-29 wenzelm 2010-04-29 'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29 wenzelm 2010-04-29 adapted ProofContext.infer_type;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-29 wenzelm 2010-04-29 avoid clash with keyword 'write';
2010-04-29 wenzelm 2010-04-29 allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-29 wenzelm 2010-04-29 uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
2010-04-28 wenzelm 2010-04-28 disabled spurious invocation of (interactive) sledgehammer;
2010-04-28 wenzelm 2010-04-28 merged
2010-04-28 blanchet 2010-04-28 make Mirabelle happy
2010-04-28 blanchet 2010-04-28 remove removed option
2010-04-28 blanchet 2010-04-28 merge
2010-04-28 blanchet 2010-04-28 parentheses around nested cases
2010-04-28 blanchet 2010-04-28 merged
2010-04-28 blanchet 2010-04-28 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
2010-04-28 blanchet 2010-04-28 reintroduced short names for HOL->FOL constants; other parts of the code rely on these
2010-04-28 blanchet 2010-04-28 save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
2010-04-28 blanchet 2010-04-28 unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28 blanchet 2010-04-28 redo Sledgehammer proofs (and get rid of "neg_clausify")
2010-04-28 blanchet 2010-04-28 removed "sorts" option, continued
2010-04-28 blanchet 2010-04-28 remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants
2010-04-28 blanchet 2010-04-28 insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
2010-04-28 blanchet 2010-04-28 support Vampire definitions of constants as "let" constructs in Isar proofs