isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip

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
Added several functions to the signature.
2005-10-28, by mengj
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-28, by mengj
sorted lemma lists
2005-10-27, by paulson
* HOL: alternative iff syntax;
2005-10-27, by wenzelm
consts: monomorphic;
2005-10-27, by wenzelm
removed inappropriate monomorphic test;
2005-10-27, by wenzelm
replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27, by wenzelm
alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27, by wenzelm
added module Pure/General/rat.ML
2005-10-27, by haftmann
tidied away duplicate thm
2005-10-26, by paulson
EVERY;
2005-10-25, by wenzelm
traceIt: plain term;
2005-10-25, by wenzelm
val legacy = ref false;
2005-10-25, by wenzelm

less more | (0) -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle