isabelle: Graph

added unfolding(_i);
2006-01-03, by wenzelm
unparse String/AltString: escape quotes;
2006-01-03, by wenzelm
tuned;
2006-01-03, by wenzelm
avoid hardwired Trueprop;
2006-01-03, by wenzelm
added 'using' command;
2006-01-03, by wenzelm
updated;
2006-01-03, by wenzelm
added IsarImplementation;
2006-01-03, by wenzelm
updated -- lost update!?
2006-01-03, by wenzelm
* Pure/Isar: new command 'unfolding';
2006-01-03, by wenzelm
ISABELLE_USER for remote cvs access;
2006-01-02, by wenzelm
outline;
2006-01-02, by wenzelm
"The Isabelle/Isar Implementation" manual;
2006-01-02, by wenzelm
* Provers/classical: removed obsolete classical version of elim_format;
2005-12-31, by wenzelm
tuned forall_intr_vars;
2005-12-31, by wenzelm
added classical_rule, which replaces Data.make_elim;
2005-12-31, by wenzelm
explicitly reject consts *Goal*, *False*;
2005-12-31, by wenzelm
elim rules: Classical.classical_rule;
2005-12-31, by wenzelm
removed obsolete cla_dist_concl;
2005-12-31, by wenzelm
removed classical elim_format;
2005-12-31, by wenzelm
removed obsolete Provers/make_elim.ML;
2005-12-31, by wenzelm
obsolete, see classical_rule in Provers/classical.ML;
2005-12-31, by wenzelm
more robust phantomsection;
2005-12-31, by wenzelm
require cla_dist_concl, avoid assumptions about concrete syntax;
2005-12-30, by wenzelm
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
2005-12-30, by wenzelm
provide equality_name, not_name;
2005-12-30, by wenzelm
fixed final_consts;
2005-12-30, by wenzelm
provide cla_dist_concl;
2005-12-30, by wenzelm
non-PDF: phantomsection;
2005-12-30, by wenzelm
added atom keyword
2005-12-29, by haftmann
changes in code generator keywords
2005-12-29, by haftmann
adaptions to changes in code generator
2005-12-29, by haftmann
slight improvements
2005-12-29, by haftmann
slightly improved serialization
2005-12-28, by haftmann
substantial improvements in code generating
2005-12-27, by haftmann
added map_index
2005-12-27, by haftmann
tuned proofs;
2005-12-23, by wenzelm
removed obsolete atomize_old;
2005-12-23, by wenzelm
removed obsolete induct_atomize_old;
2005-12-23, by wenzelm
the "skolem" attribute and better initialization of the clause database
2005-12-23, by paulson
blacklist of prolific theorems (must be replaced by an attribute later
2005-12-23, by paulson
tidied
2005-12-23, by paulson
tuned;
2005-12-23, by wenzelm
* Provers/induct: support simultaneous goals with mutual rules;
2005-12-23, by wenzelm
induct etc.: admit multiple rules;
2005-12-23, by wenzelm
backpatching of Substring.full;
2005-12-23, by wenzelm
goal/qed: proper treatment of two levels of conjunctions;
2005-12-23, by wenzelm
Logic.mk_conjunction_list;
2005-12-23, by wenzelm
turned bicompose_no_flatten into compose_no_flatten, without elimination;
2005-12-23, by wenzelm
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
2005-12-23, by wenzelm
added mk_conjunction_list2;
2005-12-23, by wenzelm
conj_elim_precise: proper treatment of nested conjunctions;
2005-12-23, by wenzelm
Thm.compose_no_flatten;
2005-12-23, by wenzelm
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
2005-12-23, by wenzelm
is_prefix
2005-12-23, by haftmann
slight improvements
2005-12-22, by haftmann
more lemmas
2005-12-22, by nipkow
shorter proof
2005-12-22, by paulson
Tuned syntax for perm.
2005-12-22, by berghofe
new lemmas
2005-12-22, by nipkow
Fixed a use of an outdated Substring function
2005-12-22, by paulson
tuned;
2005-12-22, by wenzelm
exh_casedist2: norm_hhf_eq;
2005-12-22, by wenzelm
added bicompose_no_flatten, which refrains from
2005-12-22, by wenzelm
bicompose_proof: no_flatten;
2005-12-22, by wenzelm
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
2005-12-22, by wenzelm
Transform mutual rule into projection.
2005-12-22, by wenzelm
added Provers/project_rule.ML
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
* induct: improved treatment of mutual goals and mutual rules;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
prop_tr': proper handling of aprop marked as bound;
2005-12-22, by wenzelm
consume: expand defs in prems of concls;
2005-12-22, by wenzelm
cases: main is_proper flag;
2005-12-22, by wenzelm
auto cases: marked improper;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
CONJUNCTS2;
2005-12-22, by wenzelm
rule_context: numbered cases;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
renamed imp_cong' to imp_cong_rule;
2005-12-22, by wenzelm
mk_conjunction: proper treatment of bounds;
2005-12-22, by wenzelm
fixed has_internal;
2005-12-22, by wenzelm
Tactic.precise_conjunction_tac;
2005-12-22, by wenzelm
added locale meta_conjunction_syntax and various conjunction rules;
2005-12-22, by wenzelm
simplified setup: removed dest_concls, local_impI, conjI;
2005-12-22, by wenzelm
induct_rulify;
2005-12-22, by wenzelm
actually produce projected rules;
2005-12-22, by wenzelm
*.inducts holds all projected rules;
2005-12-22, by wenzelm
tuned;
2005-12-22, by wenzelm
tuned induct proofs;
2005-12-22, by wenzelm
mutual induct with *.inducts;
2005-12-22, by wenzelm
wf_induct_rule: consumes 1;
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
slight improvements
2005-12-21, by haftmann
slight improvements in name handling
2005-12-21, by haftmann
slight refinements
2005-12-21, by haftmann
added eq_ord
2005-12-21, by haftmann
slight clean ups
2005-12-21, by haftmann
discontinued unflat in favour of burrow and burrow_split
2005-12-21, by haftmann
new hash table module in HOL/Too/s
2005-12-21, by paulson
modified suffix for [iff] attribute
2005-12-21, by paulson
removed or modified some instances of [iff]
2005-12-21, by paulson
tuned;
2005-12-20, by wenzelm
added .cvsignore
2005-12-20, by haftmann
removed improper .cvsignore
2005-12-20, by haftmann
removed superfluos is_prefix functions
2005-12-20, by haftmann
resolved shadowing of Library.find_first
2005-12-20, by haftmann
removed infix prefix, introduces burrow
2005-12-20, by haftmann
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-20, by mengj
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-20, by mengj
made the changes according to Florian's re-arranging of
2005-12-19, by urbanc
added proofs to show that every atom-kind combination
2005-12-19, by urbanc
added thms to perm_compose (so far only composition
2005-12-19, by urbanc
tuned one comment
2005-12-19, by urbanc
fixed a bug that occured when more than one atom-type
2005-12-19, by urbanc
fixed proof
2005-12-19, by nipkow
more cleaning up - this time of the cp-instance
2005-12-18, by urbanc
improved the finite-support proof
2005-12-18, by urbanc
improved the code for showing that a type is
2005-12-18, by urbanc
simp del: empty_Collect_eq;
2005-12-17, by wenzelm
sort_distinct;
2005-12-17, by wenzelm
added sort_distinct;
2005-12-17, by wenzelm
added container-lemma fresh_eqvt
2005-12-16, by urbanc
I think the earlier version was completely broken
2005-12-16, by urbanc
tuned more proofs
2005-12-16, by urbanc
new lemmas
2005-12-16, by nipkow
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
hashing to eliminate the output of duplicate clauses
2005-12-16, by paulson
hash tables from SML/NJ
2005-12-16, by paulson
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
there was a small error in the last commit - fixed now
2005-12-15, by urbanc
tuned more proof and added in-file documentation
2005-12-15, by urbanc
improved proofs;
2005-12-15, by wenzelm
acc_induct: proper tags;
2005-12-15, by wenzelm
removed obsolete/unused setup_induction;
2005-12-15, by wenzelm
tuned the proof of transitivity/narrowing
2005-12-15, by urbanc
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
2005-12-15, by paulson
made further tunings
2005-12-15, by urbanc
Added functions to test equivalence between clauses.
2005-12-15, by mengj
ex/Sudoku.thy
2005-12-14, by webertj
deleted redundant (looping!) simprule
2005-12-14, by paulson
modified example for new clauses
2005-12-14, by paulson
removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-14, by paulson
removed unused function repeat_RS
2005-12-14, by paulson
Changed literals' ordering and the functions for sorting literals.
2005-12-14, by mengj
1. changed fol_type, it's not a string type anymore.
2005-12-14, by mengj
changed ATP input files' names and location.
2005-12-14, by mengj
Potentially infinite lists as greatest fixed-point.
2005-12-13, by wenzelm
Provers/induct: coinduct;
2005-12-13, by wenzelm
tuned proofs;
2005-12-13, by wenzelm
added HOL/Library/Coinductive_List.thy;
2005-12-13, by wenzelm
added a fresh_left lemma that contains all instantiation
2005-12-13, by urbanc
initial commit (not to be seen by the public)
2005-12-13, by urbanc
simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-13, by chaieb
deals with Suc in mod expressions
2005-12-13, by chaieb
Poplog/pml provides a proper print function already!
2005-12-13, by wenzelm
meson no longer does these examples
2005-12-13, by paulson
now generates the name "append"
2005-12-13, by paulson
removal of functional reflexivity axioms
2005-12-13, by paulson
list_of_indset now also generates code for set type.
2005-12-13, by berghofe
added generic name mangler
2005-12-12, by haftmann
improvement in eq handling
2005-12-12, by haftmann
improvements in class and eq handling
2005-12-12, by haftmann
added dummy 'print' to non-polyml systems
2005-12-12, by haftmann
ISAR-fied some proofs
2005-12-11, by urbanc
completed the sn proof and changed the manual
2005-12-11, by urbanc
changed the types in accordance with Florian's changes
2005-12-10, by urbanc
substantial improvements for class code generation
2005-12-09, by haftmann
improved extraction interface
2005-12-09, by haftmann
tuned
2005-12-09, by urbanc
oriented result pairs in PureThy
2005-12-09, by haftmann
tuned;
2005-12-08, by wenzelm
removed Syntax.deskolem;
2005-12-08, by wenzelm
swap: no longer pervasive;
2005-12-08, by wenzelm
replaced swap by contrapos_np;
2005-12-08, by wenzelm
tuned proofs;
2005-12-08, by wenzelm
Cla.swap;
2005-12-08, by wenzelm
removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08, by wenzelm
tuned sources and proofs
2005-12-08, by wenzelm
Classical.swap;
2005-12-08, by wenzelm
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-12-08, by wenzelm
Adapted to new type of PureThy.add_defs_i.
2005-12-08, by berghofe
replaced swap by Classical.swap;
2005-12-07, by wenzelm
avoid unportable tail;
2005-12-07, by wenzelm
tuned
2005-12-07, by urbanc
removed thms 'swap' and 'nth_map' from ML toplevel
2005-12-06, by haftmann
improved serialization of classes to haskell
2005-12-06, by haftmann
improved class handling
2005-12-06, by haftmann
added 'dig' combinator
2005-12-06, by haftmann
re-oriented some result tuples in PureThy
2005-12-06, by haftmann
Added more functions for new type embedding of HOL clauses.
2005-12-06, by mengj
Added new type embedding methods for translating HOL clauses.
2005-12-06, by mengj
added code to say that discrete types (nat, bool, char)
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
transitivity should be now in a reasonable state. But
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
ISAR-fied two proofs
2005-12-05, by urbanc
Adapted to new type of store_thmss(_atts).
2005-12-05, by berghofe
Added store_thmss_atts to signature again.
2005-12-05, by berghofe
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
added an Isar-proof for the abs_ALL lemma
2005-12-04, by urbanc
tuning
2005-12-04, by urbanc
defines: beta/eta contract lhs;
2005-12-02, by wenzelm
asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-12-02, by wenzelm
mixfix_args: 1 for binders;
2005-12-02, by wenzelm
removed fixed_tr: now handled in syntax module;
2005-12-02, by wenzelm
added mixfixT;
2005-12-02, by wenzelm
defs: beta/eta contract lhs;
2005-12-02, by wenzelm
abs_def: beta/eta contract lhs;
2005-12-02, by wenzelm
Added recdef congruence rules for bounded quantifiers and commonly used
2005-12-02, by krauss
various improvements
2005-12-02, by haftmann
adjusted to improved code generator interface
2005-12-02, by haftmann
added perhaps option combinator
2005-12-02, by haftmann
adopted keyword for code generator
2005-12-02, by haftmann
Factored out proof for normalization of applications (norm_list).
2005-12-02, by berghofe
introduced new map2, fold
2005-12-02, by haftmann
typo
2005-12-01, by kleing
simprocs: static evaluation of simpset;
2005-12-01, by wenzelm
tuned;
2005-12-01, by wenzelm
tuned msg;
2005-12-01, by wenzelm
ProofContext.lthms_containing: suppress obvious duplicates;
2005-12-01, by wenzelm
unfold_tac: static evaluation of simpset;
2005-12-01, by wenzelm
superceded by timestart|stop.bash;
2005-12-01, by wenzelm
cpu time = user + system;
2005-12-01, by wenzelm
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
2005-12-01, by wenzelm
assoc_consts and assoc_types now check number of arguments in template.
2005-12-01, by berghofe
Added new component "sorts" to record datatype_info.
2005-12-01, by berghofe
timestop - report timing based on environment (cf. timestart.bash);
2005-12-01, by wenzelm
timestart - setup bash environment for timing;
2005-12-01, by wenzelm
Improved norm_proof to handle proofs containing term (type) variables
2005-12-01, by berghofe
restoring the old status of subset_refl
2005-12-01, by paulson
oriented pairs theory * 'a to 'a * theory
2005-12-01, by haftmann
initial cleanup to use the new induction method
2005-12-01, by urbanc
cleaned up further the proofs (diamond still needs work);
2005-12-01, by urbanc
changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-12-01, by urbanc
match_bind(_i): return terms;
2005-11-30, by wenzelm
method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-30, by wenzelm
simulaneous 'def';
2005-11-30, by wenzelm
added facilities to prove the pt and fs instances
2005-11-30, by urbanc
started to change the transitivity/narrowing case:
2005-11-30, by urbanc
changed everything until the interesting transitivity_narrowing
2005-11-30, by urbanc
minor improvements
2005-11-30, by haftmann
modified almost everything for the new nominal_induct
2005-11-30, by urbanc
Changed order of predicate arguments and quantifiers in strong induction rule.
2005-11-30, by berghofe
fixed the lemma where the new names generated by nominal_induct
2005-11-30, by urbanc
added one clause for substitution in the lambda-case and
2005-11-30, by urbanc
added rename_params_rule: recover orginal fresh names in subgoals/cases;
2005-11-30, by wenzelm
changed induction principle and everything to conform with the
2005-11-30, by urbanc
fresh: frees instead of terms, rename corresponding params in rule;
2005-11-30, by wenzelm
adapted to the new nominal_induction
2005-11-30, by urbanc
changed \<sim> of permutation equality to \<triangleq>
2005-11-30, by urbanc
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
2005-11-30, by wenzelm
reimplement Case expression pattern matching to support lazy patterns
2005-11-30, by huffman
add definitions as defs, not axioms
2005-11-30, by huffman
changed section names
2005-11-30, by huffman
add xsymbol syntax for u type constructor
2005-11-30, by huffman
add constant unit_when
2005-11-30, by huffman
proper treatment of tuple/tuple_fun -- nest to the left!
2005-11-30, by wenzelm
moved nth_list to Pure/library.ML;
2005-11-29, by wenzelm
added nth_list;
2005-11-29, by wenzelm
added mk_split;
2005-11-29, by wenzelm
changed the order of the induction variable and the context
2005-11-29, by urbanc
reworked version with proper support for defs, fixes, fresh specification;
2005-11-29, by wenzelm
added haskell serializer
2005-11-29, by haftmann
exported customized syntax interface
2005-11-29, by haftmann
Corrected atom class constraints in strong induction rule.
2005-11-29, by berghofe
made some of the theorem look-ups static (by using
2005-11-29, by urbanc
added (curried) fold2
2005-11-28, by haftmann
added proof of measure_induct_rule;
2005-11-28, by wenzelm
Added flags for setting and detecting whether a problem needs combinators.
2005-11-28, by mengj
Only output types if !keep_types is true.
2005-11-28, by mengj
Added two functions for CNF translation, used by other files.
2005-11-28, by mengj
Added in four control flags for HOL and FOL translations.
2005-11-28, by mengj
Slight modification to trace information.
2005-11-28, by mengj
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
2005-11-28, by mengj
Only output arities and class relations if !ResClause.keep_types is true.
2005-11-28, by mengj
some small tuning
2005-11-28, by urbanc
ISAR-fied two proofs about equality for abstraction functions.
2005-11-28, by urbanc
* Provers/induct: obtain pattern;
2005-11-27, by wenzelm
added an authors section (please let me know if somebody is left out or unhappy)
2005-11-27, by urbanc
some minor tunings
2005-11-27, by urbanc
added the version of nominal.thy that contains
2005-11-27, by urbanc
cleaned up all examples so that they work with the
2005-11-27, by urbanc
finished cleaning up the parts that collect
2005-11-27, by urbanc
Corrected treatment of non-recursive abstraction types.
2005-11-26, by berghofe
tuned induct proofs;
2005-11-25, by wenzelm
induct: insert defs in object-logic form;
2005-11-25, by wenzelm
tuned induct proofs;
2005-11-25, by wenzelm
tuned induct proofs;
2005-11-25, by wenzelm
consume: unfold defs in all major prems;
2005-11-25, by wenzelm
revert_skolem: fall back on Syntax.deskolem;
2005-11-25, by wenzelm
forall_conv ~1;
2005-11-25, by wenzelm
added dummy_pattern;
2005-11-25, by wenzelm
tuned names;
2005-11-25, by wenzelm
forall_conv: limit prefix;
2005-11-25, by wenzelm
fix_tac: proper treatment of major premises in goal;
2005-11-25, by wenzelm
removed obsolete dummy paragraphs;
2005-11-25, by wenzelm
tuned;
2005-11-25, by wenzelm
code generator: case expressions, improved name resolving
2005-11-25, by haftmann
added fsub.thy (poplmark challenge) to the examples
2005-11-25, by urbanc
Fixed problem with strong induction theorem for datatypes containing
2005-11-25, by berghofe
send more information with test-takes-too-long message
2005-11-25, by kleing
fixed spelling of 'case_conclusion';
2005-11-24, by wenzelm
tuned induct proofs;
2005-11-24, by wenzelm
tuned induction proofs;
2005-11-23, by wenzelm
more robust revert_skolem;
2005-11-23, by wenzelm
tuned;
2005-11-23, by wenzelm
Provers/induct: definitional insts and fixing;
2005-11-23, by wenzelm
consume: proper treatment of defs;
2005-11-23, by wenzelm
added case_conclusion attribute;
2005-11-23, by wenzelm
(co)induct: taking;
2005-11-23, by wenzelm
RuleCases.case_conclusion;
2005-11-23, by wenzelm
tuned;
2005-11-23, by wenzelm
added case_conclusion attribute;
2005-11-23, by wenzelm
improved failure tracking
2005-11-23, by haftmann
Datatype_Universe: hide base names only;
2005-11-22, by wenzelm
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
2005-11-22, by wenzelm
cases_tactic;
2005-11-22, by wenzelm
moved multi_resolve(s) to drule.ML;
2005-11-22, by wenzelm
find_xxxS: term instead of thm;
2005-11-22, by wenzelm
export map_tags;
2005-11-22, by wenzelm
make coinduct actually work;
2005-11-22, by wenzelm
Drule.multi_resolves;
2005-11-22, by wenzelm
declare coinduct rule;
2005-11-22, by wenzelm
added code generator syntax
2005-11-22, by haftmann
added codegenerator
2005-11-22, by haftmann
added code generator syntax
2005-11-22, by haftmann
new treatment of polymorphic types, using Sign.const_typargs
2005-11-22, by paulson
added codegen package
2005-11-21, by haftmann
added serializer
2005-11-21, by haftmann
tweak
2005-11-21, by paulson
fixed some inconveniencies in website
2005-11-21, by haftmann
CONJUNCTS;
2005-11-19, by wenzelm
tuned;
2005-11-19, by wenzelm
Goal.norm_hhf_protected;
2005-11-19, by wenzelm
added coinduct attribute;
2005-11-19, by wenzelm
added CONJUNCTS: treat conjunction as separate sub-goals;
2005-11-19, by wenzelm
simpset: added reorient field, set_reorient;
2005-11-19, by wenzelm
tuned norm_hhf_protected;
2005-11-19, by wenzelm
removed conj_mono;
2005-11-19, by wenzelm
induct: CONJUNCTS for multiple goals;
2005-11-19, by wenzelm
tuned induct syntax;
2005-11-19, by wenzelm
FOL: -p 2;
2005-11-19, by wenzelm
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-11-18, by chaieb
-- changed the interface of functions vampire_oracle and eprover_oracle.
2005-11-18, by mengj
-- terms are fully typed.
2005-11-18, by mengj
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-18, by 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.
2005-11-18, by mengj
-- added combinator reduction axioms (typed and untyped) for HOL goals.
2005-11-18, by mengj
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
2005-11-18, by mengj
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-11-18, by mengj
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
2005-11-18, by mengj
tuned document;
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
improved induction proof: local defs/fixes;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added deskolem;
2005-11-16, by wenzelm
added THEN_ALL_NEW_CASES;
2005-11-16, by wenzelm
added revert_skolem, mk_def, add_def;
2005-11-16, by wenzelm
ProofContext.mk_def;
2005-11-16, by wenzelm
Term.betapplys;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added betapplys;
2005-11-16, by wenzelm
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
norm_hhf: no normalization of protected props;
2005-11-16, by wenzelm
added protect_cong, cong_mono_thm;
2005-11-16, by wenzelm
induct: support local definitions to be passed through the induction;
2005-11-16, by wenzelm
Trueprop: use ObjectLogic.judgment etc.;
2005-11-16, by wenzelm
Term.betapply;
2005-11-16, by wenzelm
new version of "tryres" allowing multiple unifiers (apparently needed for
2005-11-16, by paulson
pgmlsymbolson: append Symbol.xsymbolsN at end!
2005-11-16, by wenzelm
better no -d option;
2005-11-15, by wenzelm
added generic transformators
2005-11-15, by haftmann
removal of is_hol
2005-11-14, by paulson
added module system
2005-11-14, by haftmann
added modules for code generator generation two, not operational yet
2005-11-14, by haftmann
class_package - operational view on type classes
2005-11-14, by haftmann
string_of_alist - convenient q'n'd printout function
2005-11-14, by haftmann
support for polyml-4.2.0;
2005-11-14, by wenzelm
new syntax for class_package
2005-11-14, by haftmann
added const_instance;
2005-11-14, by wenzelm
added instance;
2005-11-14, by wenzelm
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
2005-11-14, by wenzelm
Compatibility wrapper for Poly/ML 4.2.0.
2005-11-14, by wenzelm
tuned;
2005-11-14, by wenzelm
added a few equivariance lemmas (they need to be automated
2005-11-14, by urbanc
changed the HOL_basic_ss back and selectively added
2005-11-13, by urbanc
exchanged HOL_ss for HOL_basic_ss in the simplification
2005-11-13, by urbanc
a proof step corrected due to the changement in the presburger method.
2005-11-11, by chaieb
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
2005-11-11, by chaieb
add header
2005-11-11, by huffman
tuned proofs;
2005-11-10, by wenzelm
moved find_free to term.ML;
2005-11-10, by wenzelm
guess: Seq.hd;
2005-11-10, by wenzelm
guess: Toplevel.proof;
2005-11-10, by wenzelm
added find_free (from Isar/proof_context.ML);
2005-11-10, by wenzelm
curried multiply;
2005-11-10, by wenzelm
induct method: fixes;
2005-11-10, by wenzelm
uncurried Consts.typargs;
2005-11-10, by wenzelm
renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-10, by wenzelm
duplicate axioms in ATP linkup, and general fixes
2005-11-10, by paulson
tidying
2005-11-10, by paulson
called the induction principle "unsafe" instead of "test".
2005-11-10, by urbanc
Skolemization by inference, but not quite finished
2005-11-09, by paulson
Explicit data structures for some Isar language elements.
2005-11-09, by wenzelm
tuned;
2005-11-09, by wenzelm
tvars_intr_list: natural argument order;
2005-11-09, by wenzelm
moved datatype elem to element.ML;
2005-11-09, by wenzelm
P.context_element, P.locale_element;
2005-11-09, by wenzelm
Element.context;
2005-11-09, by wenzelm
use existing exeption Empty;
2005-11-09, by wenzelm
avoid code redundancy;
2005-11-09, by wenzelm
tuned comments;
2005-11-09, by wenzelm
removed obsolete term set operations;
2005-11-09, by wenzelm
P.locale_element;
2005-11-09, by wenzelm
added fold_terms;
2005-11-09, by wenzelm
added Isar/element.ML;
2005-11-09, by wenzelm
Thm.varifyT': natural argument order;
2005-11-09, by wenzelm
added join function
2005-11-09, by haftmann
allowing indentation of 'theory' keyword
2005-11-08, by haftmann
simplified after_qed;
2005-11-08, by wenzelm
avoid prove_plain, export_plain, simplified after_qed;
2005-11-08, by wenzelm
removed export_plain;
2005-11-08, by wenzelm
renamed assert_prop to ensure_prop;
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
export compose_hhf;
2005-11-08, by wenzelm
removed impose_hyps, satisfy_hyps;
2005-11-08, by wenzelm
const args: do not store variable names (unused);
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
(fix for accidental commit)
2005-11-08, by haftmann
(codegen)
2005-11-08, by haftmann
generate pattern combinators for new datatypes
2005-11-08, by huffman
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07, by huffman
add case syntax for type one
2005-11-07, by huffman
remove syntax for as-patterns
2005-11-07, by huffman
avoid 'as' as identifier;
2005-11-07, by wenzelm
avoid 'as' as identifier;
2005-11-07, by wenzelm
Added strong induction theorem (currently only axiomatized!).
2005-11-07, by berghofe
Initial commit.
2005-11-07, by urbanc
Initial commit of the theory "Weakening".
2005-11-07, by urbanc
added thms perm, distinct and fresh to the simplifier.
2005-11-07, by urbanc
added proper fillin_mixfix
2005-11-07, by haftmann
added fillin_mixfix, replace_quote
2005-11-07, by haftmann
New function store_thmss_atts.
2005-11-07, by berghofe
used the function Library.product for the cprod from Stefan
2005-11-07, by urbanc
fixed bug with nominal induct
2005-11-07, by urbanc
added fillin_mixfix' needed by serializer
2005-11-07, by haftmann
add case syntax stuff
2005-11-06, by huffman
use consts for infix syntax
2005-11-06, by huffman
add proof of Bekic's theorem: fix_cprod
2005-11-06, by huffman
simplify definitions
2005-11-05, by huffman
put iterate and fix in separate sections; added Letrec
2005-11-05, by huffman
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-05, by huffman
add line breaks to Rep_CFun syntax
2005-11-05, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
2005-11-04, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy
2005-11-04, by huffman
cleaned up
2005-11-04, by huffman
add print translation: Abs_CFun f => LAM x. f x
2005-11-04, by huffman
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
2005-11-03, by mengj
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
2005-11-03, by huffman
reimplement copy_def to use data constructor constants
2005-11-03, by huffman
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
2005-11-03, by huffman
generate lambda pattern syntax for new data constructors
2005-11-03, by huffman
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
2005-11-03, by huffman
add constant one_when; LAM pattern for ONE
2005-11-03, by huffman
add translation for wildcard pattern
2005-11-03, by huffman
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03, by huffman
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
2005-11-03, by huffman
cleaned up; ch2ch_Rep_CFun is a simp rule
2005-11-03, by huffman
changed iterate to a continuous type
2005-11-03, by huffman
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
2005-11-03, by huffman
removed ex/loeckx.ML
2005-11-03, by huffman
removed proof about Ifix, which no longer exists
2005-11-03, by huffman
cleaned up; chain_const and thelub_const are simp rules
2005-11-03, by huffman
cleaned up; removed adm_tricks in favor of compactness theorems
2005-11-03, by huffman
fix spelling
2005-11-02, by huffman