src/HOL/Proofs/ex/XML_Data.thy
Mon, 04 Nov 2019 15:15:56 +0100 wenzelm tuned;
Mon, 04 Nov 2019 15:14:34 +0100 wenzelm updated xml_size;
Sun, 20 Oct 2019 20:38:22 +0200 wenzelm clarified expand_proof/expand_name: allow more detailed control via thm_header;
Sun, 20 Oct 2019 16:16:23 +0200 wenzelm option to export standardized proof terms (not scalable);
Fri, 11 Oct 2019 21:51:10 +0200 wenzelm clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
Fri, 04 Oct 2019 15:30:52 +0200 wenzelm Term_XML.Encode/Decode.term uses Const "typargs";
Tue, 30 Jul 2019 20:09:25 +0200 wenzelm clarified global theory context;
Tue, 30 Jul 2019 11:41:39 +0200 wenzelm clarified modules;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Sat, 04 Feb 2017 21:15:11 +0100 wenzelm more uniform use of Reconstruct.clean_proof_of;
Sat, 09 Apr 2016 13:28:32 +0200 wenzelm clarified context;
Wed, 30 Dec 2015 18:25:39 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 28 Aug 2015 11:53:09 +0200 wenzelm tuned signature;
Tue, 02 Jun 2015 10:12:29 +0200 wenzelm clarified context;
Wed, 29 Apr 2015 23:30:47 +0200 wenzelm use smaller example that fits into 64MB string limit of Poly/ML x86 platform;
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
Fri, 12 Jul 2013 21:13:57 +0200 wenzelm more robust proof export / import due to Stefan Berghofer;
Sun, 23 Jun 2013 16:47:45 +0200 wenzelm support for XML data representation of proof terms;
less more (0) tip