src/HOL/Tools/BNF/bnf_lift.ML
17 months ago wenzelm 2017-11-26 more symbols;
21 months ago traytel 2017-07-11 store the unfolded definitions of the lifted bnf constants under "_def" name
2016-04-19 traytel 2016-04-19 unfold internal definitions before emitting a proof obligation
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-03-31 traytel 2016-03-31 tuned interface
2016-03-22 blanchet 2016-03-22 nicer error
2016-03-14 blanchet 2016-03-14 generalized ML function
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-12 traytel 2016-01-12 more careful witness' type analysis
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-08-31 wenzelm 2015-08-31 misc tuning and simplification;
2015-08-31 wenzelm 2015-08-31 proper option, not catch-all pattern;
2015-08-31 wenzelm 2015-08-31 misc tuning and clarification;
2015-08-13 traytel 2015-08-13 unfold intermediate definitions (stemming from composition) in lifted bnf operations
2015-08-12 traytel 2015-08-12 new command for lifting BNF structure over typedefs