src/Pure/pure_thy.ML
changeset 63609 be0a4a0bf7f5
parent 62789 ce15dd971965
child 64556 851ae0e7b09c
     1.1 --- a/src/Pure/pure_thy.ML	Thu Aug 04 21:25:16 2016 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Aug 04 21:30:20 2016 +0200
     1.3 @@ -223,7 +223,6 @@
     1.4        \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
     1.5      (Binding.make ("conjunction_def", @{here}),
     1.6        prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
     1.7 -  #> Global_Theory.add_thmss [((Binding.make ("nothing", @{here}), []), [])] #> snd
     1.8    #> fold (fn (a, prop) =>
     1.9        snd o Thm.add_axiom_global (Binding.make (a, @{here}), prop)) Proofterm.equality_axms);
    1.10