src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
Tue, 05 Jul 2016 17:52:08 +0200 blanchet tuning
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Sat, 11 Jun 2016 16:41:11 +0200 wenzelm clarified syntax;
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Tue, 31 May 2016 11:54:45 +0200 blanchet made parsing of monomorphic/polymorphic constants more robust
Tue, 31 May 2016 10:53:11 +0200 blanchet more flexible parsing (towards type class support)
Mon, 30 May 2016 14:15:44 +0200 wenzelm allow 'for' fixes for multi_specs;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Sun, 17 Apr 2016 20:54:17 +0200 wenzelm prefer binding over base name;
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Tue, 29 Mar 2016 19:17:05 +0200 blanchet tuning
Tue, 29 Mar 2016 18:07:55 +0200 blanchet more natural order for 'cong_intros'
Tue, 29 Mar 2016 10:57:02 +0200 blanchet renamed generated theorem
Mon, 28 Mar 2016 12:05:47 +0200 blanchet avoid 'prove_sorry' for unreliable tactics
Mon, 28 Mar 2016 12:05:47 +0200 blanchet reused code
Mon, 28 Mar 2016 12:05:47 +0200 blanchet tuning
Mon, 28 Mar 2016 12:05:47 +0200 blanchet more reliable check for rhs variables
Wed, 23 Mar 2016 16:37:13 +0100 blanchet sorted out type issue with sort constraints
Tue, 22 Mar 2016 12:39:37 +0100 blanchet moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
less more (0) tip