add translation for wildcard pattern

change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

cleaned up; ch2ch_Rep_CFun is a simp rule

changed iterate to a continuous type

reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less

removed ex/loeckx.ML

removed proof about Ifix, which no longer exists

cleaned up; chain_const and thelub_const are simp rules

cleaned up; removed adm_tricks in favor of compactness theorems

fix spelling

Moved atom stuff to new file nominal_atoms.ML

- completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names

Added code for proving that new datatype has finite support.

removed unused modify_typargs, map_typargs, fold_typargs;

added Isar.state/exn;

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;