Sat, 17 Mar 2012 16:13:41 +0100 | wenzelm | merged | changeset | files |
Sat, 17 Mar 2012 12:37:32 +0000 | paulson | merged | changeset | files |
Sat, 17 Mar 2012 12:36:11 +0000 | paulson | tidying and structured proofs | changeset | files |
Sat, 17 Mar 2012 16:07:03 +0100 | wenzelm | refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; | changeset | files |
Sat, 17 Mar 2012 15:33:08 +0100 | wenzelm | tuned proofs; | changeset | files |
Sat, 17 Mar 2012 14:01:09 +0100 | wenzelm | simultaneous read_fields -- e.g. relevant for sort assignment; | changeset | files |
Sat, 17 Mar 2012 13:06:23 +0100 | wenzelm | added Syntax.read_typs; | changeset | files |