2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-05-04 blanchet 2011-05-04 [mq]: nitpick_tuning
2011-05-04 blanchet 2011-05-04 fixed cardinality computation for function types such as "'a -> unit"
2011-05-04 blanchet 2011-05-04 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
2011-05-04 wenzelm 2011-05-04 proper case_names for int_cases, int_of_nat_induct; tuned some proofs, eliminating (cases, auto) anti-pattern;
2011-05-04 blanchet 2011-05-04 added type annotation for SML/NJ
2011-05-04 blanchet 2011-05-04 eta-expansion for SML/NJ
2011-05-03 wenzelm 2011-05-03 removed odd historical material;
2011-05-03 wenzelm 2011-05-03 merged
2011-05-03 blanchet 2011-05-03 fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
2011-05-03 blanchet 2011-05-03 cosmetics
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-05-03 wenzelm 2011-05-03 railsetup required for IsarRef/style;
2011-05-03 wenzelm 2011-05-03 fit page;
2011-05-03 wenzelm 2011-05-03 use existing \<hyphen>;
2011-05-03 wenzelm 2011-05-03 more precise syntax diagram;
2011-05-03 wenzelm 2011-05-03 simplified rail configuration;
2011-05-03 wenzelm 2011-05-03 provide \isabellestyle{itunderscore} (requires underscore.sty);
2011-05-03 wenzelm 2011-05-03 updated generated files;
2011-05-03 wenzelm 2011-05-03 proper treatment of empty name -- avoid excessive vertical space;
2011-05-03 wenzelm 2011-05-03 final \makeatother -- catcodes appear to be global;
2011-05-03 blanchet 2011-05-03 fixed long name truncation logic
2011-05-03 wenzelm 2011-05-03 some documentation of @{rail} antiquotation;
2011-05-03 wenzelm 2011-05-03 more precise source position for @{rail};
2011-05-03 wenzelm 2011-05-03 sane paragraph layout;
2011-05-03 wenzelm 2011-05-03 updated configuration options -- no ML here;
2011-05-03 wenzelm 2011-05-03 tag ML as in IsarImplementation;
2011-05-03 wenzelm 2011-05-03 treat underscore as in IsarRef;
2011-05-03 wenzelm 2011-05-03 reactivated codegen example based on Lambda.thy;
2011-05-03 wenzelm 2011-05-03 formal Base theory;
2011-05-03 blanchet 2011-05-03 reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
2011-05-03 blanchet 2011-05-03 whitespace tuning
2011-05-03 blanchet 2011-05-03 make SML/NJ happiest
2011-05-03 blanchet 2011-05-03 no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet 2011-05-02 do not declare TPTP built-ins, e.g. $true
2011-05-02 blanchet 2011-05-02 SNARK workaround
2011-05-02 blanchet 2011-05-02 better default type systems for SNARK and ToFoF
2011-05-02 blanchet 2011-05-02 tuning
2011-05-02 blanchet 2011-05-02 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
2011-05-02 blanchet 2011-05-02 generate tags for simps, intros, and elims in TPTP poblems on demand
2011-05-02 blanchet 2011-05-02 proper default for TPTP source filed
2011-05-02 blanchet 2011-05-02 have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-02 wenzelm 2011-05-02 eliminated old CVS Ids;
2011-05-02 wenzelm 2011-05-02 no use of package rail;
2011-05-02 wenzelm 2011-05-02 obsolete;
2011-05-02 wenzelm 2011-05-02 removed rail garbage;
2011-05-02 wenzelm 2011-05-02 NEWS;
2011-05-02 wenzelm 2011-05-02 just one railsetup.sty which is shipped with the official distribution to accompany @{rail} in Pure;
2011-05-02 wenzelm 2011-05-02 proper treatment of underscore in rail diagrams;
2011-05-02 wenzelm 2011-05-02 simplified rail setup, using plain defaults (NB: \small is incompatible with \isabellestyle used here);
2011-05-02 wenzelm 2011-05-02 eliminated external rail executable;
2011-05-02 wenzelm 2011-05-02 removed obsolete rail diagrams (which were about old-style theory syntax);
2011-05-02 wenzelm 2011-05-02 moved material about old codegen to isar-ref manual; eliminated old rail diagram;
2011-05-02 wenzelm 2011-05-02 eliminated some duplicate "def" positions;
2011-05-02 wenzelm 2011-05-02 'axiomatization' is global;
2011-05-02 wenzelm 2011-05-02 discontinued old version of old HOL manual;
2011-05-02 wenzelm 2011-05-02 merged
2011-05-02 wenzelm 2011-05-02 removed obsolete rail setup;
2011-05-02 wenzelm 2011-05-02 uniform content markup;