isabelle: Graph

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
Moved atom stuff to new file nominal_atoms.ML
2005-11-02, by berghofe
- completed the list of thms for supp_atm
2005-11-02, by urbanc
Added code for proving that new datatype has finite support.
2005-11-02, by berghofe
removed unused modify_typargs, map_typargs, fold_typargs;
2005-11-02, by wenzelm
added Isar.state/exn;
2005-11-02, by wenzelm
Isar.loop;
2005-11-02, by wenzelm
moved consts declarations to consts.ML;
2005-11-02, by wenzelm
Consts.dest;
2005-11-02, by wenzelm
Polymorphic constants.
2005-11-02, by wenzelm
added consts.ML;
2005-11-02, by wenzelm
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
2005-11-02, by wenzelm
dist_eqI: the_context();
2005-11-02, by wenzelm
Sign.const_monomorphic;
2005-11-02, by wenzelm
Logic.nth_prem;
2005-11-02, by wenzelm
added the collection of lemmas "supp_at"
2005-11-02, by urbanc
some minor tweaks in some proofs (nothing extraordinary)
2005-11-01, by urbanc
tunings of some comments (nothing serious)
2005-11-01, by urbanc
nth_*, fold_index refined
2005-10-31, by haftmann
fold_index replacing foldln
2005-10-31, by haftmann
A few new lemmas
2005-10-31, by nipkow
tuned my last commit
2005-10-30, by urbanc
simplified the abs_supp_approx proof and tuned some comments in
2005-10-30, by urbanc
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
2005-10-29, by urbanc
1) have adjusted the swapping of the result type
2005-10-29, by urbanc
tuned;
2005-10-28, by wenzelm
lthms_containing: not o valid_thms;
2005-10-28, by wenzelm
added fact_tac, some_fact_tac;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added fact method;
2005-10-28, by wenzelm
tuned ProofContext.export interfaces;
2005-10-28, by wenzelm
syntax for literal facts;
2005-10-28, by wenzelm
removed try_dest_Goal, use Logic.unprotect;
2005-10-28, by wenzelm
added cgoal_of;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
export cong_modifiers, simp_modifiers';
2005-10-28, by wenzelm
certify_term: tuned monomorphic consts;
2005-10-28, by wenzelm
datatype thmref: added Fact;
2005-10-28, by wenzelm
Logic.lift_all;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added add_local/add_global;
2005-10-28, by wenzelm
added incr_indexes;
2005-10-28, by wenzelm
renamed Goal constant to prop;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
Logic.unprotect;
2005-10-28, by wenzelm
literal facts;
2005-10-28, by wenzelm
* Pure/Isar: literal facts;
2005-10-28, by wenzelm
tuned;
2005-10-28, by wenzelm
unnecessary imports removed
2005-10-28, by webertj
fixed case names in the weak induction principle and
2005-10-28, by urbanc
Implemented proof of weak induction theorem.
2005-10-28, by berghofe
Added "deepen" method.
2005-10-28, by berghofe
circumvented smlnj value restriction
2005-10-28, by haftmann
added extraction interface for code generator
2005-10-28, by haftmann
Added (optional) arguments to the tactics
2005-10-28, by urbanc
cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28, by haftmann
Removed legacy prove_goalw_cterm command.
2005-10-28, by berghofe
got rid of obsolete prove_goalw_cterm
2005-10-28, by paulson
swapped add_datatype result
2005-10-28, by haftmann
removed obfuscating PStrStrTab
2005-10-28, by haftmann
reachable - abandoned foldl_map in favor of fold_map
2005-10-28, by haftmann
Added Tools/res_hol_clause.ML
2005-10-28, by mengj
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-28, by mengj
Added "writeln_strs" to the signature
2005-10-28, by mengj
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28, by mengj
Added new functions to handle HOL goals and lemmas.
2005-10-28, by mengj
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
2005-10-28, by mengj