Isar.loop;

moved consts declarations to consts.ML;

Consts.dest;

Polymorphic constants.

added consts.ML;

fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;

dist_eqI: the_context();

Sign.const_monomorphic;

Logic.nth_prem;

added the collection of lemmas "supp_at"

some minor tweaks in some proofs (nothing extraordinary)

tunings of some comments (nothing serious)

nth_*, fold_index refined

fold_index replacing foldln

A few new lemmas

tuned my last commit

simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML

Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.

1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")

tuned;

lthms_containing: not o valid_thms;

added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces;

added fact method; accomodate simplified Thm.lift_rule;

tuned ProofContext.export interfaces;

syntax for literal facts;

removed try_dest_Goal, use Logic.unprotect;

added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;

accomodate simplified Thm.lift_rule; tuned;

export cong_modifiers, simp_modifiers';

certify_term: tuned monomorphic consts;

datatype thmref: added Fact; renamed Goal constant to prop;

Logic.lift_all;

renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;

renamed Goal.norm_hhf_rule to Goal.norm_hhf;

renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all;

added add_local/add_global; index props (for add_local only); added could_unify;

added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;

renamed Goal constant to prop;

accomodate simplified Thm.lift_rule;

Logic.unprotect;

literal facts;

* Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;

tuned;

unnecessary imports removed

fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"

Implemented proof of weak induction theorem.

Added "deepen" method.

circumvented smlnj value restriction

added extraction interface for code generator

Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.

cleaned up nth, nth_update, nth_map and nth_string functions

Removed legacy prove_goalw_cterm command.

got rid of obsolete prove_goalw_cterm

swapped add_datatype result

removed obfuscating PStrStrTab

reachable - abandoned foldl_map in favor of fold_map

Added Tools/res_hol_clause.ML

Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.