| 2015-10-13 |
haftmann |
2015-10-13 |
prod_case as canonical name for product type eliminator
|
file | diff | annotate |
| 2015-07-26 |
wenzelm |
2015-07-26 |
updated to infer_instantiate;
clarified context;
|
file | diff | annotate |
| 2015-07-18 |
wenzelm |
2015-07-18 |
prefer tactics with explicit context;
|
file | diff | annotate |
| 2015-05-30 |
wenzelm |
2015-05-30 |
tuned -- more direct Thm.renamed_prop;
|
file | diff | annotate |
| 2015-04-08 |
wenzelm |
2015-04-08 |
proper context for Object_Logic operations;
|
file | diff | annotate |
| 2015-03-06 |
wenzelm |
2015-03-06 |
clarified context;
|
file | diff | annotate |
| 2015-03-06 |
wenzelm |
2015-03-06 |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file | diff | annotate |
| 2015-03-04 |
wenzelm |
2015-03-04 |
tuned signature -- prefer qualified names;
|
file | diff | annotate |
| 2015-03-03 |
traytel |
2015-03-03 |
eliminated some clones of Proof_Context.cterm_of
|
file | diff | annotate |
| 2014-11-26 |
wenzelm |
2014-11-26 |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file | diff | annotate |
| 2014-11-09 |
wenzelm |
2014-11-09 |
proper context for match_tac etc.;
|
file | diff | annotate |
| 2014-08-19 |
wenzelm |
2014-08-19 |
simplified type Proof.method;
|
file | diff | annotate |
| 2014-03-06 |
wenzelm |
2014-03-06 |
tuned;
|
file | diff | annotate |
| 2013-12-14 |
wenzelm |
2013-12-14 |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
|
file | diff | annotate |
| 2013-08-23 |
wenzelm |
2013-08-23 |
tuned signature;
|
file | diff | annotate |
| 2013-07-27 |
wenzelm |
2013-07-27 |
standardized aliases;
|
file | diff | annotate |
| 2013-04-18 |
wenzelm |
2013-04-18 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| 2011-11-03 |
wenzelm |
2011-11-03 |
tuned signature;
|
file | diff | annotate |
| 2011-10-12 |
wenzelm |
2011-10-12 |
tuned signature;
|
file | diff | annotate |
| 2011-04-27 |
wenzelm |
2011-04-27 |
reorganized fixes as specialized (global) name space;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
modernized structure Proof_Context;
|
file | diff | annotate |
| 2010-05-26 |
haftmann |
2010-05-26 |
dropped legacy theorem bindings
|
file | diff | annotate |
| 2010-05-17 |
wenzelm |
2010-05-17 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
|
file | diff | annotate |
| 2010-01-10 |
berghofe |
2010-01-10 |
Added infrastructure for simplifying equality constraints.
Option (no_simp) restores old behaviour of induct method.
|
file | diff | annotate |
| 2009-11-25 |
haftmann |
2009-11-25 |
normalized uncurry take/drop
|
file | diff | annotate |
| 2009-11-24 |
haftmann |
2009-11-24 |
curried take/drop
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
modernized structure Rule_Cases;
|
file | diff | annotate |
| 2009-10-15 |
wenzelm |
2009-10-15 |
replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;
|
file | diff | annotate |
| 2009-03-16 |
wenzelm |
2009-03-16 |
simplified method setup;
|
file | diff | annotate |
| 2009-03-13 |
wenzelm |
2009-03-13 |
unified type Proof.method and pervasive METHOD combinators;
|
file | diff | annotate |
| 2009-02-25 |
berghofe |
2009-02-25 |
Added lemmas for normalizing freshness results involving fresh_star.
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-09-02 |
wenzelm |
2008-09-02 |
explicit type Name.binding for higher-specification elements;
|
file | diff | annotate |
| 2008-08-09 |
wenzelm |
2008-08-09 |
unified Args.T with OuterLex.token, renamed some operations;
|
file | diff | annotate |
| 2008-06-26 |
wenzelm |
2008-06-26 |
Args.context;
|
file | diff | annotate |
| 2008-05-18 |
wenzelm |
2008-05-18 |
guess_instance: proper context;
|
file | diff | annotate |
| 2008-04-17 |
wenzelm |
2008-04-17 |
adapted to ProofContext.revert_skolem: extra Name.clean required;
|
file | diff | annotate |
| 2008-01-26 |
wenzelm |
2008-01-26 |
avoid redundant escaping of Isabelle symbols;
|
file | diff | annotate |
| 2007-10-09 |
wenzelm |
2007-10-09 |
generic Syntax.pretty/string_of operations;
|
file | diff | annotate |
| 2007-10-04 |
wenzelm |
2007-10-04 |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file | diff | annotate |
| 2007-07-05 |
wenzelm |
2007-07-05 |
simplified ObjectLogic.atomize;
|
file | diff | annotate |
| 2007-01-16 |
urbanc |
2007-01-16 |
added capabilities to handle mutual inductions
|
file | diff | annotate |
| 2006-12-18 |
haftmann |
2006-12-18 |
switched argument order in *.syntax lifters
|
file | diff | annotate |
| 2006-10-12 |
urbanc |
2006-10-12 |
To be consistent with "induct", I renamed "fixing" to "arbitrary".
However I am not very fond of "arbitrary" - e.g. it clashes with
"arbitrary" of HOL. Both Gentzen (at least in the Szabo translation)
and Velleman (in How to prove it: a structured approach) use
"arbitrary".
Still, I wonder whether "generalising" is a good compromise?
|
file | diff | annotate |
| 2006-08-02 |
wenzelm |
2006-08-02 |
simplified Assumption/ProofContext.export;
|
file | diff | annotate |
| 2006-07-11 |
wenzelm |
2006-07-11 |
Name.internal;
|
file | diff | annotate |
| 2006-06-17 |
wenzelm |
2006-06-17 |
RuleCases.mutual_rule: ctxt;
Term.internal;
ProofContext.exports: simultaneous facts;
|
file | diff | annotate |
| 2006-02-21 |
wenzelm |
2006-02-21 |
distinct (op =);
removed spurious PolyML.print;
|
file | diff | annotate |
| 2006-02-13 |
berghofe |
2006-02-13 |
Adapted to Context.generic syntax.
|
file | diff | annotate |
| 2006-01-07 |
wenzelm |
2006-01-07 |
RuleCases.make_nested;
|
file | diff | annotate |
| 2006-01-05 |
wenzelm |
2006-01-05 |
proper handling of simultaneous goals and mutual rules;
|
file | diff | annotate |
| 2005-12-01 |
urbanc |
2005-12-01 |
changed "fresh:" to "avoiding:" and cleaned up the weakening example
|
file | diff | annotate |
| 2005-11-30 |
wenzelm |
2005-11-30 |
added rename_params_rule: recover orginal fresh names in subgoals/cases;
|
file | diff | annotate |
| 2005-11-30 |
wenzelm |
2005-11-30 |
fresh: frees instead of terms, rename corresponding params in rule;
tuned;
|
file | diff | annotate |
| 2005-11-30 |
wenzelm |
2005-11-30 |
proper treatment of tuple/tuple_fun -- nest to the left!
|
file | diff | annotate |
| 2005-11-29 |
wenzelm |
2005-11-29 |
reworked version with proper support for defs, fixes, fresh specification;
|
file | diff | annotate |
| 2005-11-27 |
urbanc |
2005-11-27 |
some minor tunings
|
file | diff | annotate |
| 2005-11-13 |
urbanc |
2005-11-13 |
changed the HOL_basic_ss back and selectively added
simp_thms and triv_forall_equality. (Otherwise the
goals would have been simplified too much)
|
file | diff | annotate |
| 2005-11-13 |
urbanc |
2005-11-13 |
exchanged HOL_ss for HOL_basic_ss in the simplification
part. Otherwise the case where the context is instantiated
with unit leads to vacuous quantifiers, such as
ALL a. A
|
file | diff | annotate |