| Mon, 28 Nov 2005 00:25:43 +0100 |
urbanc |
ISAR-fied two proofs about equality for abstraction functions.
|
changeset |
files
|
| Sun, 27 Nov 2005 20:06:24 +0100 |
wenzelm |
* Provers/induct: obtain pattern;
|
changeset |
files
|
| Sun, 27 Nov 2005 06:01:11 +0100 |
urbanc |
added an authors section (please let me know if somebody is left out or unhappy)
|
changeset |
files
|
| Sun, 27 Nov 2005 05:09:43 +0100 |
urbanc |
some minor tunings
|
changeset |
files
|
| Sun, 27 Nov 2005 05:00:43 +0100 |
urbanc |
added the version of nominal.thy that contains
|
changeset |
files
|
| Sun, 27 Nov 2005 04:59:20 +0100 |
urbanc |
cleaned up all examples so that they work with the
|
changeset |
files
|
| Sun, 27 Nov 2005 03:55:16 +0100 |
urbanc |
finished cleaning up the parts that collect
|
changeset |
files
|
| Sat, 26 Nov 2005 18:41:41 +0100 |
berghofe |
Corrected treatment of non-recursive abstraction types.
|
changeset |
files
|
| Fri, 25 Nov 2005 21:14:34 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 20:57:51 +0100 |
wenzelm |
induct: insert defs in object-logic form;
|
changeset |
files
|
| Fri, 25 Nov 2005 19:20:56 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 19:09:44 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:43 +0100 |
wenzelm |
consume: unfold defs in all major prems;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:42 +0100 |
wenzelm |
revert_skolem: fall back on Syntax.deskolem;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:41 +0100 |
wenzelm |
forall_conv ~1;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:40 +0100 |
wenzelm |
added dummy_pattern;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:38 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:37 +0100 |
wenzelm |
forall_conv: limit prefix;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:36 +0100 |
wenzelm |
fix_tac: proper treatment of major premises in goal;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:35 +0100 |
wenzelm |
removed obsolete dummy paragraphs;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 25 Nov 2005 17:41:52 +0100 |
haftmann |
code generator: case expressions, improved name resolving
|
changeset |
files
|
| Fri, 25 Nov 2005 14:51:39 +0100 |
urbanc |
added fsub.thy (poplmark challenge) to the examples
|
changeset |
files
|
| Fri, 25 Nov 2005 14:00:22 +0100 |
berghofe |
Fixed problem with strong induction theorem for datatypes containing
|
changeset |
files
|
| Fri, 25 Nov 2005 11:34:37 +0100 |
kleing |
send more information with test-takes-too-long message
|
changeset |
files
|
| Thu, 24 Nov 2005 12:14:56 +0100 |
wenzelm |
fixed spelling of 'case_conclusion';
|
changeset |
files
|
| Thu, 24 Nov 2005 00:00:20 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
changeset |
files
|
| Wed, 23 Nov 2005 22:23:52 +0100 |
wenzelm |
more robust revert_skolem;
|
changeset |
files
|
| Wed, 23 Nov 2005 20:29:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:05 +0100 |
wenzelm |
Provers/induct: definitional insts and fixing;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:04 +0100 |
wenzelm |
consume: proper treatment of defs;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:03 +0100 |
wenzelm |
added case_conclusion attribute;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:02 +0100 |
wenzelm |
(co)induct: taking;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:01 +0100 |
wenzelm |
RuleCases.case_conclusion;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:51:59 +0100 |
wenzelm |
added case_conclusion attribute;
|
changeset |
files
|
| Wed, 23 Nov 2005 17:16:42 +0100 |
haftmann |
improved failure tracking
|
changeset |
files
|
| Tue, 22 Nov 2005 19:37:36 +0100 |
wenzelm |
Datatype_Universe: hide base names only;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:50 +0100 |
wenzelm |
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:48 +0100 |
wenzelm |
cases_tactic;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:47 +0100 |
wenzelm |
moved multi_resolve(s) to drule.ML;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:46 +0100 |
wenzelm |
find_xxxS: term instead of thm;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:44 +0100 |
wenzelm |
export map_tags;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:43 +0100 |
wenzelm |
make coinduct actually work;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:41 +0100 |
wenzelm |
Drule.multi_resolves;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:40 +0100 |
wenzelm |
declare coinduct rule;
|
changeset |
files
|
| Tue, 22 Nov 2005 14:32:01 +0100 |
haftmann |
added code generator syntax
|
changeset |
files
|
| Tue, 22 Nov 2005 12:59:25 +0100 |
haftmann |
added codegenerator
|
changeset |
files
|
| Tue, 22 Nov 2005 12:42:59 +0100 |
haftmann |
added code generator syntax
|
changeset |
files
|
| Tue, 22 Nov 2005 10:09:11 +0100 |
paulson |
new treatment of polymorphic types, using Sign.const_typargs
|
changeset |
files
|
| Mon, 21 Nov 2005 16:51:57 +0100 |
haftmann |
added codegen package
|
changeset |
files
|
| Mon, 21 Nov 2005 15:15:32 +0100 |
haftmann |
added serializer
|
changeset |
files
|
| Mon, 21 Nov 2005 11:14:11 +0100 |
paulson |
tweak
|
changeset |
files
|
| Mon, 21 Nov 2005 10:44:14 +0100 |
haftmann |
fixed some inconveniencies in website
|
changeset |
files
|
| Sat, 19 Nov 2005 14:22:28 +0100 |
wenzelm |
CONJUNCTS;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:09 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:08 +0100 |
wenzelm |
Goal.norm_hhf_protected;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:07 +0100 |
wenzelm |
added coinduct attribute;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:06 +0100 |
wenzelm |
added CONJUNCTS: treat conjunction as separate sub-goals;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:05 +0100 |
wenzelm |
simpset: added reorient field, set_reorient;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:04 +0100 |
wenzelm |
tuned norm_hhf_protected;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:03 +0100 |
wenzelm |
removed conj_mono;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:02 +0100 |
wenzelm |
induct: CONJUNCTS for multiple goals;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:01 +0100 |
wenzelm |
tuned induct syntax;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:00 +0100 |
wenzelm |
FOL: -p 2;
|
changeset |
files
|
| Fri, 18 Nov 2005 07:13:58 +0100 |
chaieb |
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
|
changeset |
files
|
| Fri, 18 Nov 2005 07:10:37 +0100 |
mengj |
-- changed the interface of functions vampire_oracle and eprover_oracle.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:10:00 +0100 |
mengj |
-- terms are fully typed.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:54 +0100 |
mengj |
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:18 +0100 |
mengj |
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:47 +0100 |
mengj |
-- added combinator reduction axioms (typed and untyped) for HOL goals.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:06 +0100 |
mengj |
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
|
changeset |
files
|
| Fri, 18 Nov 2005 07:06:07 +0100 |
mengj |
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:05:11 +0100 |
mengj |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
|
changeset |
files
|
| Wed, 16 Nov 2005 19:34:19 +0100 |
wenzelm |
tuned document;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:50:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:49:16 +0100 |
wenzelm |
improved induction proof: local defs/fixes;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:36 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:35 +0100 |
wenzelm |
added deskolem;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:34 +0100 |
wenzelm |
added THEN_ALL_NEW_CASES;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:33 +0100 |
wenzelm |
added revert_skolem, mk_def, add_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:32 +0100 |
wenzelm |
ProofContext.mk_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:31 +0100 |
wenzelm |
Term.betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:29 +0100 |
wenzelm |
added betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:28 +0100 |
wenzelm |
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:26 +0100 |
wenzelm |
norm_hhf: no normalization of protected props;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:25 +0100 |
wenzelm |
added protect_cong, cong_mono_thm;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:24 +0100 |
wenzelm |
induct: support local definitions to be passed through the induction;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:23 +0100 |
wenzelm |
Trueprop: use ObjectLogic.judgment etc.;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:22 +0100 |
wenzelm |
Term.betapply;
|
changeset |
files
|
| Wed, 16 Nov 2005 15:29:23 +0100 |
paulson |
new version of "tryres" allowing multiple unifiers (apparently needed for
|
changeset |
files
|
| Wed, 16 Nov 2005 14:05:41 +0100 |
wenzelm |
pgmlsymbolson: append Symbol.xsymbolsN at end!
|
changeset |
files
|
| Tue, 15 Nov 2005 14:08:32 +0100 |
wenzelm |
better no -d option;
|
changeset |
files
|
| Tue, 15 Nov 2005 10:11:52 +0100 |
haftmann |
added generic transformators
|
changeset |
files
|
| Mon, 14 Nov 2005 18:25:34 +0100 |
paulson |
removal of is_hol
|
changeset |
files
|
| Mon, 14 Nov 2005 16:26:40 +0100 |
haftmann |
added module system
|
changeset |
files
|
| Mon, 14 Nov 2005 15:23:33 +0100 |
haftmann |
added modules for code generator generation two, not operational yet
|
changeset |
files
|
| Mon, 14 Nov 2005 15:15:34 +0100 |
haftmann |
class_package - operational view on type classes
|
changeset |
files
|
| Mon, 14 Nov 2005 15:15:07 +0100 |
haftmann |
string_of_alist - convenient q'n'd printout function
|
changeset |
files
|
| Mon, 14 Nov 2005 15:14:59 +0100 |
wenzelm |
support for polyml-4.2.0;
|
changeset |
files
|
| Mon, 14 Nov 2005 15:14:32 +0100 |
haftmann |
new syntax for class_package
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:48 +0100 |
wenzelm |
added const_instance;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:38 +0100 |
wenzelm |
added instance;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:15 +0100 |
wenzelm |
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:36:46 +0100 |
wenzelm |
Compatibility wrapper for Poly/ML 4.2.0.
|
changeset |
files
|
| Mon, 14 Nov 2005 14:36:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Nov 2005 13:59:58 +0100 |
urbanc |
added a few equivariance lemmas (they need to be automated
|
changeset |
files
|
| Sun, 13 Nov 2005 22:36:30 +0100 |
urbanc |
changed the HOL_basic_ss back and selectively added
|
changeset |
files
|
| Sun, 13 Nov 2005 20:33:36 +0100 |
urbanc |
exchanged HOL_ss for HOL_basic_ss in the simplification
|
changeset |
files
|
| Fri, 11 Nov 2005 10:50:43 +0100 |
chaieb |
a proof step corrected due to the changement in the presburger method.
|
changeset |
files
|
| Fri, 11 Nov 2005 10:49:59 +0100 |
chaieb |
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
|
changeset |
files
|
| Fri, 11 Nov 2005 00:09:37 +0100 |
huffman |
add header
|
changeset |
files
|
| Thu, 10 Nov 2005 21:14:05 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:22 +0100 |
wenzelm |
moved find_free to term.ML;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:21 +0100 |
wenzelm |
guess: Seq.hd;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:20 +0100 |
wenzelm |
guess: Toplevel.proof;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:19 +0100 |
wenzelm |
added find_free (from Isar/proof_context.ML);
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:18 +0100 |
wenzelm |
curried multiply;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:17 +0100 |
wenzelm |
induct method: fixes;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:16 +0100 |
wenzelm |
uncurried Consts.typargs;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
changeset |
files
|
| Thu, 10 Nov 2005 17:33:14 +0100 |
paulson |
duplicate axioms in ATP linkup, and general fixes
|
changeset |
files
|
| Thu, 10 Nov 2005 17:31:44 +0100 |
paulson |
tidying
|
changeset |
files
|
| Thu, 10 Nov 2005 00:36:26 +0100 |
urbanc |
called the induction principle "unsafe" instead of "test".
|
changeset |
files
|
| Wed, 09 Nov 2005 18:01:33 +0100 |
paulson |
Skolemization by inference, but not quite finished
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:55 +0100 |
wenzelm |
Explicit data structures for some Isar language elements.
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:53 +0100 |
wenzelm |
tvars_intr_list: natural argument order;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:52 +0100 |
wenzelm |
moved datatype elem to element.ML;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:51 +0100 |
wenzelm |
P.context_element, P.locale_element;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:50 +0100 |
wenzelm |
Element.context;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:49 +0100 |
wenzelm |
use existing exeption Empty;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:48 +0100 |
wenzelm |
avoid code redundancy;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:47 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:46 +0100 |
wenzelm |
removed obsolete term set operations;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:45 +0100 |
wenzelm |
P.locale_element;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:44 +0100 |
wenzelm |
added fold_terms;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:43 +0100 |
wenzelm |
added Isar/element.ML;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:41 +0100 |
wenzelm |
Thm.varifyT': natural argument order;
|
changeset |
files
|
| Wed, 09 Nov 2005 12:21:05 +0100 |
haftmann |
added join function
|
changeset |
files
|
| Tue, 08 Nov 2005 15:26:35 +0100 |
haftmann |
allowing indentation of 'theory' keyword
|
changeset |
files
|
| Tue, 08 Nov 2005 10:44:40 +0100 |
wenzelm |
simplified after_qed;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:15 +0100 |
wenzelm |
avoid prove_plain, export_plain, simplified after_qed;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:13 +0100 |
wenzelm |
removed export_plain;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:12 +0100 |
wenzelm |
renamed assert_prop to ensure_prop;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:11 +0100 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:10 +0100 |
wenzelm |
export compose_hhf;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:09 +0100 |
wenzelm |
removed impose_hyps, satisfy_hyps;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:08 +0100 |
wenzelm |
const args: do not store variable names (unused);
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:05 +0100 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
changeset |
files
|
| Tue, 08 Nov 2005 09:13:22 +0100 |
haftmann |
(fix for accidental commit)
|
changeset |
files
|
| Tue, 08 Nov 2005 09:12:02 +0100 |
haftmann |
(codegen)
|
changeset |
files
|
| Tue, 08 Nov 2005 02:19:11 +0100 |
huffman |
generate pattern combinators for new datatypes
|
changeset |
files
|
| Mon, 07 Nov 2005 23:33:01 +0100 |
huffman |
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
|
changeset |
files
|
| Mon, 07 Nov 2005 23:30:49 +0100 |
huffman |
add case syntax for type one
|
changeset |
files
|
| Mon, 07 Nov 2005 19:23:53 +0100 |
huffman |
remove syntax for as-patterns
|
changeset |
files
|
| Mon, 07 Nov 2005 19:03:02 +0100 |
wenzelm |
avoid 'as' as identifier;
|
changeset |
files
|
| Mon, 07 Nov 2005 18:50:53 +0100 |
wenzelm |
avoid 'as' as identifier;
|
changeset |
files
|
| Mon, 07 Nov 2005 18:32:54 +0100 |
berghofe |
Added strong induction theorem (currently only axiomatized!).
|
changeset |
files
|
| Mon, 07 Nov 2005 15:19:03 +0100 |
urbanc |
Initial commit.
|
changeset |
files
|
| Mon, 07 Nov 2005 15:12:13 +0100 |
urbanc |
Initial commit of the theory "Weakening".
|
changeset |
files
|
| Mon, 07 Nov 2005 14:35:25 +0100 |
urbanc |
added thms perm, distinct and fresh to the simplifier.
|
changeset |
files
|
| Mon, 07 Nov 2005 12:06:11 +0100 |
haftmann |
added proper fillin_mixfix
|
changeset |
files
|
| Mon, 07 Nov 2005 11:39:24 +0100 |
haftmann |
added fillin_mixfix, replace_quote
|
changeset |
files
|
| Mon, 07 Nov 2005 11:28:34 +0100 |
berghofe |
New function store_thmss_atts.
|
changeset |
files
|
| Mon, 07 Nov 2005 11:17:45 +0100 |
urbanc |
used the function Library.product for the cprod from Stefan
|
changeset |
files
|
| Mon, 07 Nov 2005 10:47:25 +0100 |
urbanc |
fixed bug with nominal induct
|
changeset |
files
|
| Mon, 07 Nov 2005 09:34:51 +0100 |
haftmann |
added fillin_mixfix' needed by serializer
|
changeset |
files
|
| Sun, 06 Nov 2005 01:21:37 +0100 |
huffman |
add case syntax stuff
|
changeset |
files
|
| Sun, 06 Nov 2005 00:35:24 +0100 |
huffman |
use consts for infix syntax
|
changeset |
files
|
| Sun, 06 Nov 2005 00:22:03 +0100 |
huffman |
add proof of Bekic's theorem: fix_cprod
|
changeset |
files
|
| Sat, 05 Nov 2005 21:56:45 +0100 |
huffman |
simplify definitions
|
changeset |
files
|
| Sat, 05 Nov 2005 21:52:13 +0100 |
huffman |
put iterate and fix in separate sections; added Letrec
|
changeset |
files
|
| Sat, 05 Nov 2005 21:50:37 +0100 |
huffman |
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
|
changeset |
files
|
| Sat, 05 Nov 2005 21:42:24 +0100 |
huffman |
add line breaks to Rep_CFun syntax
|
changeset |
files
|
| Fri, 04 Nov 2005 23:15:45 +0100 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
|
changeset |
files
|
| Fri, 04 Nov 2005 23:15:11 +0100 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy
|
changeset |
files
|
| Fri, 04 Nov 2005 22:27:40 +0100 |
huffman |
cleaned up
|
changeset |
files
|
| Fri, 04 Nov 2005 22:26:09 +0100 |
huffman |
add print translation: Abs_CFun f => LAM x. f x
|
changeset |
files
|
| Thu, 03 Nov 2005 04:31:12 +0100 |
mengj |
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
|
changeset |
files
|
| Thu, 03 Nov 2005 03:06:02 +0100 |
huffman |
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
|
changeset |
files
|
| Thu, 03 Nov 2005 02:37:09 +0100 |
huffman |
reimplement copy_def to use data constructor constants
|
changeset |
files
|
| Thu, 03 Nov 2005 02:19:48 +0100 |
huffman |
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
|
changeset |
files
|
| Thu, 03 Nov 2005 01:54:51 +0100 |
huffman |
generate lambda pattern syntax for new data constructors
|
changeset |
files
|
| Thu, 03 Nov 2005 01:45:52 +0100 |
huffman |
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
|
changeset |
files
|
| Thu, 03 Nov 2005 01:44:27 +0100 |
huffman |
add constant one_when; LAM pattern for ONE
|
changeset |
files
|
| Thu, 03 Nov 2005 01:28:22 +0100 |
huffman |
add translation for wildcard pattern
|
changeset |
files
|
| Thu, 03 Nov 2005 01:11:39 +0100 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
changeset |
files
|
| Thu, 03 Nov 2005 01:02:29 +0100 |
huffman |
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
|
changeset |
files
|
| Thu, 03 Nov 2005 00:57:35 +0100 |
huffman |
cleaned up; ch2ch_Rep_CFun is a simp rule
|
changeset |
files
|
| Thu, 03 Nov 2005 00:43:50 +0100 |
huffman |
changed iterate to a continuous type
|
changeset |
files
|
| Thu, 03 Nov 2005 00:43:11 +0100 |
huffman |
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
|
changeset |
files
|
| Thu, 03 Nov 2005 00:32:47 +0100 |
huffman |
removed ex/loeckx.ML
|
changeset |
files
|
| Thu, 03 Nov 2005 00:31:32 +0100 |
huffman |
removed proof about Ifix, which no longer exists
|
changeset |
files
|
| Thu, 03 Nov 2005 00:16:09 +0100 |
huffman |
cleaned up; chain_const and thelub_const are simp rules
|
changeset |
files
|
| Thu, 03 Nov 2005 00:12:29 +0100 |
huffman |
cleaned up; removed adm_tricks in favor of compactness theorems
|
changeset |
files
|
| Wed, 02 Nov 2005 23:59:49 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Wed, 02 Nov 2005 16:37:39 +0100 |
berghofe |
Moved atom stuff to new file nominal_atoms.ML
|
changeset |
files
|
| Wed, 02 Nov 2005 15:31:12 +0100 |
urbanc |
- completed the list of thms for supp_atm
|
changeset |
files
|
| Wed, 02 Nov 2005 15:05:22 +0100 |
berghofe |
Added code for proving that new datatype has finite support.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:48:55 +0100 |
wenzelm |
removed unused modify_typargs, map_typargs, fold_typargs;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:01 +0100 |
wenzelm |
added Isar.state/exn;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:00 +0100 |
wenzelm |
Isar.loop;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:58 +0100 |
wenzelm |
moved consts declarations to consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:57 +0100 |
wenzelm |
Consts.dest;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:56 +0100 |
wenzelm |
Polymorphic constants.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:54 +0100 |
wenzelm |
added consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:53 +0100 |
wenzelm |
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:51 +0100 |
wenzelm |
dist_eqI: the_context();
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:49 +0100 |
wenzelm |
Sign.const_monomorphic;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:47 +0100 |
wenzelm |
Logic.nth_prem;
|
changeset |
files
|
| Wed, 02 Nov 2005 11:02:29 +0100 |
urbanc |
added the collection of lemmas "supp_at"
|
changeset |
files
|
| Tue, 01 Nov 2005 23:55:53 +0100 |
urbanc |
some minor tweaks in some proofs (nothing extraordinary)
|
changeset |
files
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
changeset |
files
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
changeset |
files
|
| Mon, 31 Oct 2005 16:00:15 +0100 |
haftmann |
fold_index replacing foldln
|
changeset |
files
|
| Mon, 31 Oct 2005 01:43:22 +0100 |
nipkow |
A few new lemmas
|
changeset |
files
|
| Sun, 30 Oct 2005 10:55:56 +0100 |
urbanc |
tuned my last commit
|
changeset |
files
|
| Sun, 30 Oct 2005 10:37:57 +0100 |
urbanc |
simplified the abs_supp_approx proof and tuned some comments in
|
changeset |
files
|
| Sat, 29 Oct 2005 15:01:25 +0200 |
urbanc |
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
|
changeset |
files
|
| Sat, 29 Oct 2005 14:37:32 +0200 |
urbanc |
1) have adjusted the swapping of the result type
|
changeset |
files
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:32:55 +0200 |
wenzelm |
lthms_containing: not o valid_thms;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:15 +0200 |
wenzelm |
added fact_tac, some_fact_tac;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:13 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:12 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:11 +0200 |
wenzelm |
added fact method;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:07 +0200 |
wenzelm |
syntax for literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:06 +0200 |
wenzelm |
removed try_dest_Goal, use Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:04 +0200 |
wenzelm |
added cgoal_of;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:02 +0200 |
wenzelm |
export cong_modifiers, simp_modifiers';
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:00 +0200 |
wenzelm |
certify_term: tuned monomorphic consts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:59 +0200 |
wenzelm |
datatype thmref: added Fact;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:58 +0200 |
wenzelm |
Logic.lift_all;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|